author | wenzelm |
Wed, 25 Oct 2017 14:54:28 +0200 | |
changeset 66919 | 1f93e376aeb6 |
parent 59923 | b21c82422d65 |
child 69087 | 06017b2c4552 |
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 |
|
9 |
val experiment: Element.context_i list -> theory -> Binding.scope * local_theory |
|
10 |
val experiment_cmd: Element.context list -> theory -> Binding.scope * local_theory |
|
11 |
end; |
|
12 |
||
13 |
structure Experiment: EXPERIMENT = |
|
14 |
struct |
|
15 |
||
16 |
fun gen_experiment add_locale elems thy = |
|
17 |
let |
|
59919
fe1d8576b483
clarified name space policy: show less stuff in usual print functions;
wenzelm
parents:
59901
diff
changeset
|
18 |
val experiment_name = Binding.name ("experiment" ^ serial_string ()) |> Binding.concealed; |
fe1d8576b483
clarified name space policy: show less stuff in usual print functions;
wenzelm
parents:
59901
diff
changeset
|
19 |
val (_, lthy) = thy |> add_locale experiment_name Binding.empty ([], []) elems; |
59901 | 20 |
val (scope, naming) = |
21 |
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
|
22 |
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
|
23 |
val lthy' = lthy |
fe1d8576b483
clarified name space policy: show less stuff in usual print functions;
wenzelm
parents:
59901
diff
changeset
|
24 |
|> 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
|
25 |
|> Local_Theory.map_background_naming Name_Space.concealed; |
59901 | 26 |
in (scope, lthy') end; |
27 |
||
28 |
val experiment = gen_experiment Expression.add_locale; |
|
29 |
val experiment_cmd = gen_experiment Expression.add_locale_cmd; |
|
30 |
||
31 |
end; |