# HG changeset patch
# User wenzelm
# Date 1427918886 -7200
# Node ID 840d03805755ff895c9c8d2f30d78204b83580c7
# Parent  a5591a15112e05c730489b2a6b53d9e45b3a0787
added command 'experiment';

diff -r a5591a15112e -r 840d03805755 NEWS
--- 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.
 
diff -r a5591a15112e -r 840d03805755 src/Doc/Isar_Ref/Spec.thy
--- 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
diff -r a5591a15112e -r 840d03805755 src/Pure/Isar/experiment.ML
--- /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;
diff -r a5591a15112e -r 840d03805755 src/Pure/Isar/isar_syn.ML
--- 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
diff -r a5591a15112e -r 840d03805755 src/Pure/Pure.thy
--- 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
diff -r a5591a15112e -r 840d03805755 src/Pure/ROOT
--- 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"
diff -r a5591a15112e -r 840d03805755 src/Pure/ROOT.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";