4 Target for specification experiments that are mostly private. |
4 Target for specification experiments that are mostly private. |
5 *) |
5 *) |
6 |
6 |
7 signature EXPERIMENT = |
7 signature EXPERIMENT = |
8 sig |
8 sig |
|
9 val is_experiment: theory -> string -> bool |
9 val experiment: Element.context_i list -> theory -> Binding.scope * local_theory |
10 val experiment: Element.context_i list -> theory -> Binding.scope * local_theory |
10 val experiment_cmd: Element.context list -> theory -> Binding.scope * local_theory |
11 val experiment_cmd: Element.context list -> theory -> Binding.scope * local_theory |
11 end; |
12 end; |
12 |
13 |
13 structure Experiment: EXPERIMENT = |
14 structure Experiment: EXPERIMENT = |
14 struct |
15 struct |
15 |
16 |
|
17 structure Data = Theory_Data |
|
18 ( |
|
19 type T = Symtab.set; |
|
20 val empty = Symtab.empty; |
|
21 val extend = I; |
|
22 val merge = Symtab.merge (K true); |
|
23 ); |
|
24 |
|
25 fun is_experiment thy name = Symtab.defined (Data.get thy) name; |
|
26 |
16 fun gen_experiment add_locale elems thy = |
27 fun gen_experiment add_locale elems thy = |
17 let |
28 let |
18 val experiment_name = Binding.name ("experiment" ^ serial_string ()) |> Binding.concealed; |
29 val experiment_name = Binding.name ("experiment" ^ serial_string ()) |> Binding.concealed; |
19 val (_, lthy) = thy |> add_locale experiment_name Binding.empty ([], []) elems; |
30 val lthy = |
|
31 thy |
|
32 |> add_locale experiment_name Binding.empty ([], []) elems |
|
33 |-> (Local_Theory.background_theory o Data.map o Symtab.insert_set); |
20 val (scope, naming) = |
34 val (scope, naming) = |
21 Name_Space.new_scope (Proof_Context.naming_of (Local_Theory.target_of lthy)); |
35 Name_Space.new_scope (Proof_Context.naming_of (Local_Theory.target_of lthy)); |
22 val naming' = naming |> Name_Space.private_scope scope; |
36 val naming' = naming |> Name_Space.private_scope scope; |
23 val lthy' = lthy |
37 val lthy' = lthy |
24 |> Local_Theory.map_contexts (K (Proof_Context.map_naming (K naming'))) |
38 |> Local_Theory.map_contexts (K (Proof_Context.map_naming (K naming'))) |