author | wenzelm |
Thu, 06 Jun 2024 22:26:40 +0200 | |
changeset 80274 | cff00b3dddf5 |
parent 77723 | b761c91c2447 |
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 |
( |
77723
b761c91c2447
performance tuning: prefer functor Set() over Table();
wenzelm
parents:
74561
diff
changeset
|
19 |
type T = Symset.T; |
b761c91c2447
performance tuning: prefer functor Set() over Table();
wenzelm
parents:
74561
diff
changeset
|
20 |
val empty = Symset.empty; |
b761c91c2447
performance tuning: prefer functor Set() over Table();
wenzelm
parents:
74561
diff
changeset
|
21 |
val merge = Symset.merge; |
69087
06017b2c4552
suppress aux. locales from command 'experiment' -- avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
59923
diff
changeset
|
22 |
); |
06017b2c4552
suppress aux. locales from command 'experiment' -- avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
59923
diff
changeset
|
23 |
|
77723
b761c91c2447
performance tuning: prefer functor Set() over Table();
wenzelm
parents:
74561
diff
changeset
|
24 |
fun is_experiment thy name = Symset.member (Data.get thy) name; |
69087
06017b2c4552
suppress aux. locales from command 'experiment' -- avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
59923
diff
changeset
|
25 |
|
59901 | 26 |
fun gen_experiment add_locale elems thy = |
27 |
let |
|
59919
fe1d8576b483
clarified name space policy: show less stuff in usual print functions;
wenzelm
parents:
59901
diff
changeset
|
28 |
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
|
29 |
val lthy = |
06017b2c4552
suppress aux. locales from command 'experiment' -- avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
wenzelm
parents:
59923
diff
changeset
|
30 |
thy |
72536
589645894305
bundle mixins for locale and class specifications
haftmann
parents:
69087
diff
changeset
|
31 |
|> add_locale experiment_name Binding.empty [] ([], []) elems |
77723
b761c91c2447
performance tuning: prefer functor Set() over Table();
wenzelm
parents:
74561
diff
changeset
|
32 |
|-> (Local_Theory.background_theory o Data.map o Symset.insert); |
59901 | 33 |
val (scope, naming) = |
34 |
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
|
35 |
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
|
36 |
val lthy' = lthy |
fe1d8576b483
clarified name space policy: show less stuff in usual print functions;
wenzelm
parents:
59901
diff
changeset
|
37 |
|> 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
|
38 |
|> Local_Theory.map_background_naming Name_Space.concealed; |
59901 | 39 |
in (scope, lthy') end; |
40 |
||
41 |
val experiment = gen_experiment Expression.add_locale; |
|
42 |
val experiment_cmd = gen_experiment Expression.add_locale_cmd; |
|
43 |
||
44 |
end; |