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