--- a/src/Pure/Isar/experiment.ML Sun Sep 30 11:58:59 2018 +0200
+++ b/src/Pure/Isar/experiment.ML Sun Sep 30 12:26:14 2018 +0200
@@ -6,6 +6,7 @@
signature EXPERIMENT =
sig
+ val is_experiment: theory -> string -> bool
val experiment: Element.context_i list -> theory -> Binding.scope * local_theory
val experiment_cmd: Element.context list -> theory -> Binding.scope * local_theory
end;
@@ -13,10 +14,23 @@
structure Experiment: EXPERIMENT =
struct
+structure Data = Theory_Data
+(
+ type T = Symtab.set;
+ val empty = Symtab.empty;
+ val extend = I;
+ val merge = Symtab.merge (K true);
+);
+
+fun is_experiment thy name = Symtab.defined (Data.get thy) name;
+
fun gen_experiment add_locale elems thy =
let
val experiment_name = Binding.name ("experiment" ^ serial_string ()) |> Binding.concealed;
- val (_, lthy) = thy |> add_locale experiment_name Binding.empty ([], []) elems;
+ val lthy =
+ thy
+ |> add_locale experiment_name Binding.empty ([], []) elems
+ |-> (Local_Theory.background_theory o Data.map o Symtab.insert_set);
val (scope, naming) =
Name_Space.new_scope (Proof_Context.naming_of (Local_Theory.target_of lthy));
val naming' = naming |> Name_Space.private_scope scope;