author | wenzelm |
Sun, 30 Sep 2018 12:26:14 +0200 | |
changeset 69087 | 06017b2c4552 |
parent 59923 | b21c82422d65 |
child 72536 | 589645894305 |
permissions | -rw-r--r-- |
59901 | 1 |
(* Title: Pure/Isar/experiment.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
Target for specification experiments that are mostly private. |
|
5 |
*) |
|
6 |
||
7 |
signature EXPERIMENT = |
|
8 |
sig |
|
69087
06017b2c4552
suppress aux. locales from command 'experiment' -- avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
59923
diff
changeset
|
9 |
val is_experiment: theory -> string -> bool |
59901 | 10 |
val experiment: Element.context_i list -> theory -> Binding.scope * local_theory |
11 |
val experiment_cmd: Element.context list -> theory -> Binding.scope * local_theory |
|
12 |
end; |
|
13 |
||
14 |
structure Experiment: EXPERIMENT = |
|
15 |
struct |
|
16 |
||
69087
06017b2c4552
suppress aux. locales from command 'experiment' -- avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
59923
diff
changeset
|
17 |
structure Data = Theory_Data |
06017b2c4552
suppress aux. locales from command 'experiment' -- avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
59923
diff
changeset
|
18 |
( |
06017b2c4552
suppress aux. locales from command 'experiment' -- avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
59923
diff
changeset
|
19 |
type T = Symtab.set; |
06017b2c4552
suppress aux. locales from command 'experiment' -- avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
59923
diff
changeset
|
20 |
val empty = Symtab.empty; |
06017b2c4552
suppress aux. locales from command 'experiment' -- avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
59923
diff
changeset
|
21 |
val extend = I; |
06017b2c4552
suppress aux. locales from command 'experiment' -- avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
59923
diff
changeset
|
22 |
val merge = Symtab.merge (K true); |
06017b2c4552
suppress aux. locales from command 'experiment' -- avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
59923
diff
changeset
|
23 |
); |
06017b2c4552
suppress aux. locales from command 'experiment' -- avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
59923
diff
changeset
|
24 |
|
06017b2c4552
suppress aux. locales from command 'experiment' -- avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
59923
diff
changeset
|
25 |
fun is_experiment thy name = Symtab.defined (Data.get thy) name; |
06017b2c4552
suppress aux. locales from command 'experiment' -- avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
59923
diff
changeset
|
26 |
|
59901 | 27 |
fun gen_experiment add_locale elems thy = |
28 |
let |
|
59919
fe1d8576b483
clarified name space policy: show less stuff in usual print functions;
wenzelm
parents:
59901
diff
changeset
|
29 |
val experiment_name = Binding.name ("experiment" ^ serial_string ()) |> Binding.concealed; |
69087
06017b2c4552
suppress aux. locales from command 'experiment' -- avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
59923
diff
changeset
|
30 |
val lthy = |
06017b2c4552
suppress aux. locales from command 'experiment' -- avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
59923
diff
changeset
|
31 |
thy |
06017b2c4552
suppress aux. locales from command 'experiment' -- avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
59923
diff
changeset
|
32 |
|> add_locale experiment_name Binding.empty ([], []) elems |
06017b2c4552
suppress aux. locales from command 'experiment' -- avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
59923
diff
changeset
|
33 |
|-> (Local_Theory.background_theory o Data.map o Symtab.insert_set); |
59901 | 34 |
val (scope, naming) = |
35 |
Name_Space.new_scope (Proof_Context.naming_of (Local_Theory.target_of lthy)); |
|
59923
b21c82422d65
support private scope for individual local theory commands;
wenzelm
parents:
59919
diff
changeset
|
36 |
val naming' = naming |> Name_Space.private_scope scope; |
59919
fe1d8576b483
clarified name space policy: show less stuff in usual print functions;
wenzelm
parents:
59901
diff
changeset
|
37 |
val lthy' = lthy |
fe1d8576b483
clarified name space policy: show less stuff in usual print functions;
wenzelm
parents:
59901
diff
changeset
|
38 |
|> Local_Theory.map_contexts (K (Proof_Context.map_naming (K naming'))) |
fe1d8576b483
clarified name space policy: show less stuff in usual print functions;
wenzelm
parents:
59901
diff
changeset
|
39 |
|> Local_Theory.map_background_naming Name_Space.concealed; |
59901 | 40 |
in (scope, lthy') end; |
41 |
||
42 |
val experiment = gen_experiment Expression.add_locale; |
|
43 |
val experiment_cmd = gen_experiment Expression.add_locale_cmd; |
|
44 |
||
45 |
end; |