--- 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"}
--- 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, ...}) =
--- 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;
--- 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 *)
--- 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;
--- 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;
--- 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 =>
--- 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 == ""
--- 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;