1(* Title: Pure/Isar/experiment.ML 2 Author: Makarius 3 4Target for specification experiments that are mostly private. 5*) 6 7signature EXPERIMENT = 8sig 9 val experiment: Element.context_i list -> theory -> Binding.scope * local_theory 10 val experiment_cmd: Element.context list -> theory -> Binding.scope * local_theory 11end; 12 13structure Experiment: EXPERIMENT = 14struct 15 16fun gen_experiment add_locale elems thy = 17 let 18 val experiment_name = Binding.name ("experiment" ^ serial_string ()) |> Binding.concealed; 19 val (_, lthy) = thy |> add_locale experiment_name Binding.empty ([], []) elems; 20 val (scope, naming) = 21 Name_Space.new_scope (Proof_Context.naming_of (Local_Theory.target_of lthy)); 22 val naming' = naming |> Name_Space.private_scope scope; 23 val lthy' = lthy 24 |> Local_Theory.map_contexts (K (Proof_Context.map_naming (K naming'))) 25 |> Local_Theory.map_background_naming Name_Space.concealed; 26 in (scope, lthy') end; 27 28val experiment = gen_experiment Expression.add_locale; 29val experiment_cmd = gen_experiment Expression.add_locale_cmd; 30 31end; 32