--- a/NEWS Wed Apr 01 21:12:05 2015 +0200
+++ b/NEWS Wed Apr 01 22:08:06 2015 +0200
@@ -6,6 +6,9 @@
*** General ***
+* Command 'experiment' opens an anonymous locale context with private
+naming policy.
+
* Structural composition of proof methods (meth1; meth2) in Isar
corresponds to (tac1 THEN_ALL_NEW tac2) in ML.
--- a/src/Doc/Isar_Ref/Spec.thy Wed Apr 01 21:12:05 2015 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy Wed Apr 01 22:08:06 2015 +0200
@@ -501,6 +501,7 @@
text \<open>
\begin{matharray}{rcl}
@{command_def "locale"} & : & @{text "theory \<rightarrow> local_theory"} \\
+ @{command_def "experiment"} & : & @{text "theory \<rightarrow> local_theory"} \\
@{command_def "print_locale"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def "print_locales"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def "locale_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@@ -513,6 +514,8 @@
@{rail \<open>
@@{command locale} @{syntax name} ('=' @{syntax locale})? @'begin'?
;
+ @@{command experiment} (@{syntax context_elem}*) @'begin'
+ ;
@@{command print_locale} '!'? @{syntax nameref}
;
@{syntax_def locale}: @{syntax context_elem}+ |
@@ -610,7 +613,12 @@
@{text "\<Longrightarrow>"} by @{text "\<longrightarrow>"} in HOL; see also
\secref{sec:object-logic}). Separate introduction rules @{text
loc_axioms.intro} and @{text loc.intro} are provided as well.
-
+
+ \item @{command experiment}~@{text exprs}~@{keyword "begin"} opens an
+ anonymous locale context with private naming policy. Specifications in its
+ body are inaccessible from outside. This is useful to perform experiments,
+ without polluting the name space.
+
\item @{command "print_locale"}~@{text "locale"} prints the
contents of the named locale. The command omits @{element "notes"}
elements by default. Use @{command "print_locale"}@{text "!"} to
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/experiment.ML Wed Apr 01 22:08:06 2015 +0200
@@ -0,0 +1,29 @@
+(* Title: Pure/Isar/experiment.ML
+ Author: Makarius
+
+Target for specification experiments that are mostly private.
+*)
+
+signature EXPERIMENT =
+sig
+ 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
+
+fun gen_experiment add_locale elems thy =
+ let
+ val (_, lthy) = thy
+ |> add_locale (Binding.name ("experiment" ^ serial_string ())) Binding.empty ([], []) elems;
+ val (scope, naming) =
+ Name_Space.new_scope (Proof_Context.naming_of (Local_Theory.target_of lthy));
+ val naming' = naming |> Name_Space.private scope;
+ val lthy' = lthy |> Local_Theory.map_contexts (K (Proof_Context.map_naming (K naming')));
+ in (scope, lthy') end;
+
+val experiment = gen_experiment Expression.add_locale;
+val experiment_cmd = gen_experiment Expression.add_locale_cmd;
+
+end;
--- a/src/Pure/Isar/isar_syn.ML Wed Apr 01 21:12:05 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML Wed Apr 01 22:08:06 2015 +0200
@@ -373,13 +373,19 @@
Scan.repeat1 Parse_Spec.context_element >> pair ([], []);
val _ =
- Outer_Syntax.command @{command_spec "locale"} "define named proof context"
+ Outer_Syntax.command @{command_spec "locale"} "define named specification context"
(Parse.binding --
Scan.optional (@{keyword "="} |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
>> (fn ((name, (expr, elems)), begin) =>
Toplevel.begin_local_theory begin
(Expression.add_locale_cmd name Binding.empty expr elems #> snd)));
+val _ =
+ Outer_Syntax.command @{command_spec "experiment"} "open private specification context"
+ (Scan.repeat Parse_Spec.context_element --| Parse.begin
+ >> (fn elems =>
+ Toplevel.begin_local_theory true (Experiment.experiment_cmd elems #> snd)));
+
fun interpretation_args mandatory =
Parse.!!! (Parse_Spec.locale_expression mandatory) --
Scan.optional
--- a/src/Pure/Pure.thy Wed Apr 01 21:12:05 2015 +0200
+++ b/src/Pure/Pure.thy Wed Apr 01 22:08:06 2015 +0200
@@ -33,7 +33,7 @@
and "bundle" :: thy_decl
and "include" "including" :: prf_decl
and "print_bundles" :: diag
- and "context" "locale" :: thy_decl_block
+ and "context" "locale" "experiment" :: thy_decl_block
and "sublocale" "interpretation" :: thy_goal
and "interpret" :: prf_goal % "proof"
and "class" :: thy_decl_block
--- a/src/Pure/ROOT Wed Apr 01 21:12:05 2015 +0200
+++ b/src/Pure/ROOT Wed Apr 01 22:08:06 2015 +0200
@@ -121,6 +121,7 @@
"Isar/code.ML"
"Isar/context_rules.ML"
"Isar/element.ML"
+ "Isar/experiment.ML"
"Isar/expression.ML"
"Isar/generic_target.ML"
"Isar/isar_cmd.ML"
--- a/src/Pure/ROOT.ML Wed Apr 01 21:12:05 2015 +0200
+++ b/src/Pure/ROOT.ML Wed Apr 01 22:08:06 2015 +0200
@@ -273,6 +273,7 @@
use "Isar/expression.ML";
use "Isar/class_declaration.ML";
use "Isar/bundle.ML";
+use "Isar/experiment.ML";
use "simplifier.ML";
use "Tools/plugin.ML";