Target for specification experiments that are mostly private.
*)
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;
structure Experiment: EXPERIMENT = struct
structure Data = Theory_Data
( type T = Symset.T; val empty = Symset.empty; val merge = Symset.merge;
);
fun is_experiment thy name = Symset.member (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
|-> (Local_Theory.background_theory o Data.map o Symset.insert); val (scope, naming) =
Name_Space.new_scope (Proof_Context.naming_of (Local_Theory.target_of lthy)); val naming' = naming |> Name_Space.private_scope scope; val lthy' = lthy
|> Local_Theory.map_contexts (K (Proof_Context.map_naming (K naming')))
|> Local_Theory.map_background_naming Name_Space.concealed; in (scope, lthy') end;
val experiment = gen_experiment Expression.add_locale; val experiment_cmd = gen_experiment Expression.add_locale_cmd;
end;
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
