# HG changeset patch
# User wenzelm
# Date 1428149051 -7200
# Node ID b21c82422d6501bc577f6a4f13fca892e1f76cb1
# Parent  1b6283aa7c94080ac95ef570852c482bc88e5c6f
support private scope for individual local theory commands;
tuned signature;

diff -r 1b6283aa7c94 -r b21c82422d65 src/HOL/SPARK/Tools/spark_commands.ML
--- a/src/HOL/SPARK/Tools/spark_commands.ML	Fri Apr 03 21:25:55 2015 +0200
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Sat Apr 04 14:04:11 2015 +0200
@@ -123,7 +123,7 @@
 val _ =
   Outer_Syntax.command @{command_spec "spark_vc"}
     "enter into proof mode for a specific verification condition"
-    (Parse.name >> (fn name => Toplevel.local_theory_to_proof NONE (prove_vc name)));
+    (Parse.name >> (fn name => Toplevel.local_theory_to_proof NONE NONE (prove_vc name)));
 
 val _ =
   Outer_Syntax.command @{command_spec "spark_status"}
diff -r 1b6283aa7c94 -r b21c82422d65 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Fri Apr 03 21:25:55 2015 +0200
+++ b/src/Pure/General/name_space.ML	Sat Apr 04 14:04:11 2015 +0200
@@ -35,7 +35,8 @@
   val get_scopes: naming -> Binding.scope list
   val get_scope: naming -> Binding.scope option
   val new_scope: naming -> Binding.scope * naming
-  val private: Binding.scope -> naming -> naming
+  val private_scope: Binding.scope -> naming -> naming
+  val private: Position.T -> naming -> naming
   val concealed: naming -> naming
   val get_group: naming -> serial option
   val set_group: serial option -> naming -> naming
@@ -316,6 +317,10 @@
 fun get_scopes (Naming {scopes, ...}) = scopes;
 val get_scope = try hd o get_scopes;
 
+fun put_scope scope =
+  map_naming (fn (scopes, private, concealed, group, theory_name, path) =>
+    (scope :: scopes, private, concealed, group, theory_name, path));
+
 fun new_scope naming =
   let
     val scope = Binding.new_scope ();
@@ -324,9 +329,14 @@
         (scope :: scopes, private, concealed, group, theory_name, path));
   in (scope, naming') end;
 
-fun private scope = map_naming (fn (scopes, _, concealed, group, theory_name, path) =>
+fun private_scope scope = map_naming (fn (scopes, _, concealed, group, theory_name, path) =>
   (scopes, SOME scope, concealed, group, theory_name, path));
 
+fun private pos naming =
+  (case get_scope naming of
+    SOME scope => private_scope scope naming
+  | NONE => error ("Unknown scope -- cannot declare names private" ^ Position.here pos));
+
 val concealed = map_naming (fn (scopes, private, _, group, theory_name, path) =>
   (scopes, private, true, group, theory_name, path));
 
@@ -358,7 +368,7 @@
 (* visibility flags *)
 
 fun transform_naming (Naming {private = private', concealed = concealed', ...}) =
-  fold private (the_list private') #>
+  fold private_scope (the_list private') #>
   concealed' ? concealed;
 
 fun transform_binding (Naming {private, concealed, ...}) =
diff -r 1b6283aa7c94 -r b21c82422d65 src/Pure/Isar/experiment.ML
--- a/src/Pure/Isar/experiment.ML	Fri Apr 03 21:25:55 2015 +0200
+++ b/src/Pure/Isar/experiment.ML	Sat Apr 04 14:04:11 2015 +0200
@@ -19,7 +19,7 @@
     val (_, lthy) = thy |> add_locale experiment_name 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 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;
diff -r 1b6283aa7c94 -r b21c82422d65 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Apr 03 21:25:55 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sat Apr 04 14:04:11 2015 +0200
@@ -398,13 +398,13 @@
       interpretation_args false >> (fn (loc, (expr, equations)) =>
         Toplevel.theory_to_proof (Expression.sublocale_global_cmd loc expr equations)))
     || interpretation_args false >> (fn (expr, equations) =>
-        Toplevel.local_theory_to_proof NONE (Expression.sublocale_cmd expr equations)));
+        Toplevel.local_theory_to_proof NONE NONE (Expression.sublocale_cmd expr equations)));
 
 val _ =
   Outer_Syntax.command @{command_spec "interpretation"}
     "prove interpretation of locale expression in local theory"
     (interpretation_args true >> (fn (expr, equations) =>
-      Toplevel.local_theory_to_proof NONE (Expression.interpretation_cmd expr equations)));
+      Toplevel.local_theory_to_proof NONE NONE (Expression.interpretation_cmd expr equations)));
 
 val _ =
   Outer_Syntax.command @{command_spec "interpret"}
@@ -441,7 +441,7 @@
   ((Parse.class --
     ((@{keyword "\<subseteq>"} || @{keyword "<"}) |-- Parse.!!! Parse.class) >> Class.classrel_cmd ||
     Parse.multi_arity >> Class.instance_arity_cmd) >> Toplevel.theory_to_proof ||
-    Scan.succeed (Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I)));
+    Scan.succeed (Toplevel.local_theory_to_proof NONE NONE (Class.instantiation_instance I)));
 
 
 (* arbitrary overloading *)
diff -r 1b6283aa7c94 -r b21c82422d65 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Fri Apr 03 21:25:55 2015 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Sat Apr 04 14:04:11 2015 +0200
@@ -135,8 +135,13 @@
 fun command (name, pos) comment parse =
   Theory.setup (add_command name (new_command comment parse pos));
 
+val opt_private =
+  Scan.option (Parse.$$$ "(" |-- (Parse.position (Parse.$$$ "private") >> #2) --| Parse.$$$ ")");
+
 fun local_theory_command trans command_spec comment parse =
-  command command_spec comment (Parse.opt_target -- parse >> (fn (loc, f) => trans loc f));
+  command command_spec comment
+    (opt_private -- Parse.opt_target -- parse >>
+      (fn ((private, target), f) => trans private target f));
 
 val local_theory' = local_theory_command Toplevel.local_theory';
 val local_theory = local_theory_command Toplevel.local_theory;
diff -r 1b6283aa7c94 -r b21c82422d65 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri Apr 03 21:25:55 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sat Apr 04 14:04:11 2015 +0200
@@ -36,7 +36,8 @@
   val full_name: Proof.context -> binding -> string
   val get_scope: Proof.context -> Binding.scope option
   val new_scope: Proof.context -> Binding.scope * Proof.context
-  val private: Binding.scope -> Proof.context -> Proof.context
+  val private_scope: Binding.scope -> Proof.context -> Proof.context
+  val private: Position.T -> Proof.context -> Proof.context
   val concealed: Proof.context -> Proof.context
   val class_space: Proof.context -> Name_Space.T
   val type_space: Proof.context -> Name_Space.T
@@ -316,6 +317,7 @@
     val ctxt' = map_naming (K naming') ctxt;
   in (scope, ctxt') end;
 
+val private_scope = map_naming o Name_Space.private_scope;
 val private = map_naming o Name_Space.private;
 val concealed = map_naming Name_Space.concealed;
 
diff -r 1b6283aa7c94 -r b21c82422d65 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Fri Apr 03 21:25:55 2015 +0200
+++ b/src/Pure/Isar/toplevel.ML	Sat Apr 04 14:04:11 2015 +0200
@@ -51,15 +51,15 @@
   val end_local_theory: transition -> transition
   val open_target: (generic_theory -> local_theory) -> transition -> transition
   val close_target: transition -> transition
-  val local_theory': (xstring * Position.T) option -> (bool -> local_theory -> local_theory) ->
-    transition -> transition
-  val local_theory: (xstring * Position.T) option -> (local_theory -> local_theory) ->
-    transition -> transition
+  val local_theory': Position.T option -> (xstring * Position.T) option ->
+    (bool -> local_theory -> local_theory) -> transition -> transition
+  val local_theory: Position.T option -> (xstring * Position.T) option ->
+    (local_theory -> local_theory) -> transition -> transition
   val present_local_theory: (xstring * Position.T) option -> (state -> unit) ->
     transition -> transition
-  val local_theory_to_proof': (xstring * Position.T) option ->
+  val local_theory_to_proof': Position.T option -> (xstring * Position.T) option ->
     (bool -> local_theory -> Proof.state) -> transition -> transition
-  val local_theory_to_proof: (xstring * Position.T) option ->
+  val local_theory_to_proof: Position.T option -> (xstring * Position.T) option ->
     (local_theory -> Proof.state) -> transition -> transition
   val theory_to_proof: (theory -> Proof.state) -> transition -> transition
   val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition
@@ -412,11 +412,12 @@
         | NONE => raise UNDEF)
     | _ => raise UNDEF));
 
-fun local_theory' loc f = present_transaction (fn int =>
+fun local_theory' private target f = present_transaction (fn int =>
   (fn Theory (gthy, _) =>
         let
-          val (finish, lthy) = Named_Target.switch loc gthy;
+          val (finish, lthy) = Named_Target.switch target gthy;
           val lthy' = lthy
+            |> fold Proof_Context.private (the_list private)
             |> Local_Theory.new_group
             |> f int
             |> Local_Theory.reset_group;
@@ -424,11 +425,11 @@
     | _ => raise UNDEF))
   (K ());
 
-fun local_theory loc f = local_theory' loc (K f);
+fun local_theory private target f = local_theory' private target (K f);
 
-fun present_local_theory loc = present_transaction (fn int =>
+fun present_local_theory target = present_transaction (fn int =>
   (fn Theory (gthy, _) =>
-        let val (finish, lthy) = Named_Target.switch loc gthy;
+        let val (finish, lthy) = Named_Target.switch target gthy;
         in Theory (finish lthy, SOME lthy) end
     | _ => raise UNDEF));
 
@@ -469,12 +470,18 @@
 
 in
 
-fun local_theory_to_proof' loc f = begin_proof
+fun local_theory_to_proof' private target f = begin_proof
   (fn int => fn gthy =>
-    let val (finish, lthy) = Named_Target.switch loc gthy
-    in (finish o Local_Theory.reset_group, f int (Local_Theory.new_group lthy)) end);
+    let
+      val (finish, lthy) = Named_Target.switch target gthy;
+      val prf = lthy
+        |> fold Proof_Context.private (the_list private)
+        |> Local_Theory.new_group
+        |> f int;
+    in (finish o Local_Theory.reset_group, prf) end);
 
-fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f);
+fun local_theory_to_proof private target f =
+  local_theory_to_proof' private target (K f);
 
 fun theory_to_proof f = begin_proof
   (fn _ => fn gthy =>
diff -r 1b6283aa7c94 -r b21c82422d65 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Fri Apr 03 21:25:55 2015 +0200
+++ b/src/Pure/Pure.thy	Sat Apr 04 14:04:11 2015 +0200
@@ -11,7 +11,8 @@
     "\<subseteq>" "]" "assumes" "attach" "binder" "constrains"
     "defines" "fixes" "for" "identifier" "if" "in" "includes" "infix"
     "infixl" "infixr" "is" "notes" "obtains" "open" "output"
-    "overloaded" "pervasive" "shows" "structure" "unchecked" "where" "|"
+    "overloaded" "pervasive" "private" "shows" "structure" "unchecked"
+    "where" "|"
   and "text" "txt" :: document_body
   and "text_raw" :: document_raw
   and "default_sort" :: thy_decl == ""
diff -r 1b6283aa7c94 -r b21c82422d65 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Fri Apr 03 21:25:55 2015 +0200
+++ b/src/Pure/sign.ML	Sat Apr 04 14:04:11 2015 +0200
@@ -111,7 +111,8 @@
   val mandatory_path: string -> theory -> theory
   val qualified_path: bool -> binding -> theory -> theory
   val local_path: theory -> theory
-  val private: Binding.scope -> theory -> theory
+  val private_scope: Binding.scope -> theory -> theory
+  val private: Position.T -> theory -> theory
   val concealed: theory -> theory
   val hide_class: bool -> string -> theory -> theory
   val hide_type: bool -> string -> theory -> theory
@@ -522,6 +523,7 @@
 
 fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
 
+val private_scope = map_naming o Name_Space.private_scope;
 val private = map_naming o Name_Space.private;
 val concealed = map_naming Name_Space.concealed;