support private scope for individual local theory commands;
authorwenzelm
Sat Apr 04 14:04:11 2015 +0200 (2015-04-04 ago)
changeset 59923b21c82422d65
parent 59922 1b6283aa7c94
child 59924 801b979ec0c2
support private scope for individual local theory commands;
tuned signature;
src/HOL/SPARK/Tools/spark_commands.ML
src/Pure/General/name_space.ML
src/Pure/Isar/experiment.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/toplevel.ML
src/Pure/Pure.thy
src/Pure/sign.ML
     1.1 --- a/src/HOL/SPARK/Tools/spark_commands.ML	Fri Apr 03 21:25:55 2015 +0200
     1.2 +++ b/src/HOL/SPARK/Tools/spark_commands.ML	Sat Apr 04 14:04:11 2015 +0200
     1.3 @@ -123,7 +123,7 @@
     1.4  val _ =
     1.5    Outer_Syntax.command @{command_spec "spark_vc"}
     1.6      "enter into proof mode for a specific verification condition"
     1.7 -    (Parse.name >> (fn name => Toplevel.local_theory_to_proof NONE (prove_vc name)));
     1.8 +    (Parse.name >> (fn name => Toplevel.local_theory_to_proof NONE NONE (prove_vc name)));
     1.9  
    1.10  val _ =
    1.11    Outer_Syntax.command @{command_spec "spark_status"}
     2.1 --- a/src/Pure/General/name_space.ML	Fri Apr 03 21:25:55 2015 +0200
     2.2 +++ b/src/Pure/General/name_space.ML	Sat Apr 04 14:04:11 2015 +0200
     2.3 @@ -35,7 +35,8 @@
     2.4    val get_scopes: naming -> Binding.scope list
     2.5    val get_scope: naming -> Binding.scope option
     2.6    val new_scope: naming -> Binding.scope * naming
     2.7 -  val private: Binding.scope -> naming -> naming
     2.8 +  val private_scope: Binding.scope -> naming -> naming
     2.9 +  val private: Position.T -> naming -> naming
    2.10    val concealed: naming -> naming
    2.11    val get_group: naming -> serial option
    2.12    val set_group: serial option -> naming -> naming
    2.13 @@ -316,6 +317,10 @@
    2.14  fun get_scopes (Naming {scopes, ...}) = scopes;
    2.15  val get_scope = try hd o get_scopes;
    2.16  
    2.17 +fun put_scope scope =
    2.18 +  map_naming (fn (scopes, private, concealed, group, theory_name, path) =>
    2.19 +    (scope :: scopes, private, concealed, group, theory_name, path));
    2.20 +
    2.21  fun new_scope naming =
    2.22    let
    2.23      val scope = Binding.new_scope ();
    2.24 @@ -324,9 +329,14 @@
    2.25          (scope :: scopes, private, concealed, group, theory_name, path));
    2.26    in (scope, naming') end;
    2.27  
    2.28 -fun private scope = map_naming (fn (scopes, _, concealed, group, theory_name, path) =>
    2.29 +fun private_scope scope = map_naming (fn (scopes, _, concealed, group, theory_name, path) =>
    2.30    (scopes, SOME scope, concealed, group, theory_name, path));
    2.31  
    2.32 +fun private pos naming =
    2.33 +  (case get_scope naming of
    2.34 +    SOME scope => private_scope scope naming
    2.35 +  | NONE => error ("Unknown scope -- cannot declare names private" ^ Position.here pos));
    2.36 +
    2.37  val concealed = map_naming (fn (scopes, private, _, group, theory_name, path) =>
    2.38    (scopes, private, true, group, theory_name, path));
    2.39  
    2.40 @@ -358,7 +368,7 @@
    2.41  (* visibility flags *)
    2.42  
    2.43  fun transform_naming (Naming {private = private', concealed = concealed', ...}) =
    2.44 -  fold private (the_list private') #>
    2.45 +  fold private_scope (the_list private') #>
    2.46    concealed' ? concealed;
    2.47  
    2.48  fun transform_binding (Naming {private, concealed, ...}) =
     3.1 --- a/src/Pure/Isar/experiment.ML	Fri Apr 03 21:25:55 2015 +0200
     3.2 +++ b/src/Pure/Isar/experiment.ML	Sat Apr 04 14:04:11 2015 +0200
     3.3 @@ -19,7 +19,7 @@
     3.4      val (_, lthy) = thy |> add_locale experiment_name Binding.empty ([], []) elems;
     3.5      val (scope, naming) =
     3.6        Name_Space.new_scope (Proof_Context.naming_of (Local_Theory.target_of lthy));
     3.7 -    val naming' = naming |> Name_Space.private scope;
     3.8 +    val naming' = naming |> Name_Space.private_scope scope;
     3.9      val lthy' = lthy
    3.10        |> Local_Theory.map_contexts (K (Proof_Context.map_naming (K naming')))
    3.11        |> Local_Theory.map_background_naming Name_Space.concealed;
     4.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Apr 03 21:25:55 2015 +0200
     4.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Apr 04 14:04:11 2015 +0200
     4.3 @@ -398,13 +398,13 @@
     4.4        interpretation_args false >> (fn (loc, (expr, equations)) =>
     4.5          Toplevel.theory_to_proof (Expression.sublocale_global_cmd loc expr equations)))
     4.6      || interpretation_args false >> (fn (expr, equations) =>
     4.7 -        Toplevel.local_theory_to_proof NONE (Expression.sublocale_cmd expr equations)));
     4.8 +        Toplevel.local_theory_to_proof NONE NONE (Expression.sublocale_cmd expr equations)));
     4.9  
    4.10  val _ =
    4.11    Outer_Syntax.command @{command_spec "interpretation"}
    4.12      "prove interpretation of locale expression in local theory"
    4.13      (interpretation_args true >> (fn (expr, equations) =>
    4.14 -      Toplevel.local_theory_to_proof NONE (Expression.interpretation_cmd expr equations)));
    4.15 +      Toplevel.local_theory_to_proof NONE NONE (Expression.interpretation_cmd expr equations)));
    4.16  
    4.17  val _ =
    4.18    Outer_Syntax.command @{command_spec "interpret"}
    4.19 @@ -441,7 +441,7 @@
    4.20    ((Parse.class --
    4.21      ((@{keyword "\<subseteq>"} || @{keyword "<"}) |-- Parse.!!! Parse.class) >> Class.classrel_cmd ||
    4.22      Parse.multi_arity >> Class.instance_arity_cmd) >> Toplevel.theory_to_proof ||
    4.23 -    Scan.succeed (Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I)));
    4.24 +    Scan.succeed (Toplevel.local_theory_to_proof NONE NONE (Class.instantiation_instance I)));
    4.25  
    4.26  
    4.27  (* arbitrary overloading *)
     5.1 --- a/src/Pure/Isar/outer_syntax.ML	Fri Apr 03 21:25:55 2015 +0200
     5.2 +++ b/src/Pure/Isar/outer_syntax.ML	Sat Apr 04 14:04:11 2015 +0200
     5.3 @@ -135,8 +135,13 @@
     5.4  fun command (name, pos) comment parse =
     5.5    Theory.setup (add_command name (new_command comment parse pos));
     5.6  
     5.7 +val opt_private =
     5.8 +  Scan.option (Parse.$$$ "(" |-- (Parse.position (Parse.$$$ "private") >> #2) --| Parse.$$$ ")");
     5.9 +
    5.10  fun local_theory_command trans command_spec comment parse =
    5.11 -  command command_spec comment (Parse.opt_target -- parse >> (fn (loc, f) => trans loc f));
    5.12 +  command command_spec comment
    5.13 +    (opt_private -- Parse.opt_target -- parse >>
    5.14 +      (fn ((private, target), f) => trans private target f));
    5.15  
    5.16  val local_theory' = local_theory_command Toplevel.local_theory';
    5.17  val local_theory = local_theory_command Toplevel.local_theory;
     6.1 --- a/src/Pure/Isar/proof_context.ML	Fri Apr 03 21:25:55 2015 +0200
     6.2 +++ b/src/Pure/Isar/proof_context.ML	Sat Apr 04 14:04:11 2015 +0200
     6.3 @@ -36,7 +36,8 @@
     6.4    val full_name: Proof.context -> binding -> string
     6.5    val get_scope: Proof.context -> Binding.scope option
     6.6    val new_scope: Proof.context -> Binding.scope * Proof.context
     6.7 -  val private: Binding.scope -> Proof.context -> Proof.context
     6.8 +  val private_scope: Binding.scope -> Proof.context -> Proof.context
     6.9 +  val private: Position.T -> Proof.context -> Proof.context
    6.10    val concealed: Proof.context -> Proof.context
    6.11    val class_space: Proof.context -> Name_Space.T
    6.12    val type_space: Proof.context -> Name_Space.T
    6.13 @@ -316,6 +317,7 @@
    6.14      val ctxt' = map_naming (K naming') ctxt;
    6.15    in (scope, ctxt') end;
    6.16  
    6.17 +val private_scope = map_naming o Name_Space.private_scope;
    6.18  val private = map_naming o Name_Space.private;
    6.19  val concealed = map_naming Name_Space.concealed;
    6.20  
     7.1 --- a/src/Pure/Isar/toplevel.ML	Fri Apr 03 21:25:55 2015 +0200
     7.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Apr 04 14:04:11 2015 +0200
     7.3 @@ -51,15 +51,15 @@
     7.4    val end_local_theory: transition -> transition
     7.5    val open_target: (generic_theory -> local_theory) -> transition -> transition
     7.6    val close_target: transition -> transition
     7.7 -  val local_theory': (xstring * Position.T) option -> (bool -> local_theory -> local_theory) ->
     7.8 -    transition -> transition
     7.9 -  val local_theory: (xstring * Position.T) option -> (local_theory -> local_theory) ->
    7.10 -    transition -> transition
    7.11 +  val local_theory': Position.T option -> (xstring * Position.T) option ->
    7.12 +    (bool -> local_theory -> local_theory) -> transition -> transition
    7.13 +  val local_theory: Position.T option -> (xstring * Position.T) option ->
    7.14 +    (local_theory -> local_theory) -> transition -> transition
    7.15    val present_local_theory: (xstring * Position.T) option -> (state -> unit) ->
    7.16      transition -> transition
    7.17 -  val local_theory_to_proof': (xstring * Position.T) option ->
    7.18 +  val local_theory_to_proof': Position.T option -> (xstring * Position.T) option ->
    7.19      (bool -> local_theory -> Proof.state) -> transition -> transition
    7.20 -  val local_theory_to_proof: (xstring * Position.T) option ->
    7.21 +  val local_theory_to_proof: Position.T option -> (xstring * Position.T) option ->
    7.22      (local_theory -> Proof.state) -> transition -> transition
    7.23    val theory_to_proof: (theory -> Proof.state) -> transition -> transition
    7.24    val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition
    7.25 @@ -412,11 +412,12 @@
    7.26          | NONE => raise UNDEF)
    7.27      | _ => raise UNDEF));
    7.28  
    7.29 -fun local_theory' loc f = present_transaction (fn int =>
    7.30 +fun local_theory' private target f = present_transaction (fn int =>
    7.31    (fn Theory (gthy, _) =>
    7.32          let
    7.33 -          val (finish, lthy) = Named_Target.switch loc gthy;
    7.34 +          val (finish, lthy) = Named_Target.switch target gthy;
    7.35            val lthy' = lthy
    7.36 +            |> fold Proof_Context.private (the_list private)
    7.37              |> Local_Theory.new_group
    7.38              |> f int
    7.39              |> Local_Theory.reset_group;
    7.40 @@ -424,11 +425,11 @@
    7.41      | _ => raise UNDEF))
    7.42    (K ());
    7.43  
    7.44 -fun local_theory loc f = local_theory' loc (K f);
    7.45 +fun local_theory private target f = local_theory' private target (K f);
    7.46  
    7.47 -fun present_local_theory loc = present_transaction (fn int =>
    7.48 +fun present_local_theory target = present_transaction (fn int =>
    7.49    (fn Theory (gthy, _) =>
    7.50 -        let val (finish, lthy) = Named_Target.switch loc gthy;
    7.51 +        let val (finish, lthy) = Named_Target.switch target gthy;
    7.52          in Theory (finish lthy, SOME lthy) end
    7.53      | _ => raise UNDEF));
    7.54  
    7.55 @@ -469,12 +470,18 @@
    7.56  
    7.57  in
    7.58  
    7.59 -fun local_theory_to_proof' loc f = begin_proof
    7.60 +fun local_theory_to_proof' private target f = begin_proof
    7.61    (fn int => fn gthy =>
    7.62 -    let val (finish, lthy) = Named_Target.switch loc gthy
    7.63 -    in (finish o Local_Theory.reset_group, f int (Local_Theory.new_group lthy)) end);
    7.64 +    let
    7.65 +      val (finish, lthy) = Named_Target.switch target gthy;
    7.66 +      val prf = lthy
    7.67 +        |> fold Proof_Context.private (the_list private)
    7.68 +        |> Local_Theory.new_group
    7.69 +        |> f int;
    7.70 +    in (finish o Local_Theory.reset_group, prf) end);
    7.71  
    7.72 -fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f);
    7.73 +fun local_theory_to_proof private target f =
    7.74 +  local_theory_to_proof' private target (K f);
    7.75  
    7.76  fun theory_to_proof f = begin_proof
    7.77    (fn _ => fn gthy =>
     8.1 --- a/src/Pure/Pure.thy	Fri Apr 03 21:25:55 2015 +0200
     8.2 +++ b/src/Pure/Pure.thy	Sat Apr 04 14:04:11 2015 +0200
     8.3 @@ -11,7 +11,8 @@
     8.4      "\<subseteq>" "]" "assumes" "attach" "binder" "constrains"
     8.5      "defines" "fixes" "for" "identifier" "if" "in" "includes" "infix"
     8.6      "infixl" "infixr" "is" "notes" "obtains" "open" "output"
     8.7 -    "overloaded" "pervasive" "shows" "structure" "unchecked" "where" "|"
     8.8 +    "overloaded" "pervasive" "private" "shows" "structure" "unchecked"
     8.9 +    "where" "|"
    8.10    and "text" "txt" :: document_body
    8.11    and "text_raw" :: document_raw
    8.12    and "default_sort" :: thy_decl == ""
     9.1 --- a/src/Pure/sign.ML	Fri Apr 03 21:25:55 2015 +0200
     9.2 +++ b/src/Pure/sign.ML	Sat Apr 04 14:04:11 2015 +0200
     9.3 @@ -111,7 +111,8 @@
     9.4    val mandatory_path: string -> theory -> theory
     9.5    val qualified_path: bool -> binding -> theory -> theory
     9.6    val local_path: theory -> theory
     9.7 -  val private: Binding.scope -> theory -> theory
     9.8 +  val private_scope: Binding.scope -> theory -> theory
     9.9 +  val private: Position.T -> theory -> theory
    9.10    val concealed: theory -> theory
    9.11    val hide_class: bool -> string -> theory -> theory
    9.12    val hide_type: bool -> string -> theory -> theory
    9.13 @@ -522,6 +523,7 @@
    9.14  
    9.15  fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
    9.16  
    9.17 +val private_scope = map_naming o Name_Space.private_scope;
    9.18  val private = map_naming o Name_Space.private;
    9.19  val concealed = map_naming Name_Space.concealed;
    9.20