support for 'restricted' modifier: only qualified accesses outside the local scope;
authorwenzelm
Mon Apr 06 22:11:01 2015 +0200 (2015-04-06 ago)
changeset 599397d46aa03696e
parent 59938 f84b93187ab6
child 59940 087d81f5213e
support for 'restricted' modifier: only qualified accesses outside the local scope;
NEWS
src/Doc/Isar_Ref/Spec.thy
src/Pure/General/binding.ML
src/Pure/General/name_space.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/outer_syntax.scala
src/Pure/Isar/parse.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/token.ML
src/Pure/Isar/token.scala
src/Pure/Isar/toplevel.ML
src/Pure/Pure.thy
src/Pure/Thy/thy_output.ML
src/Pure/sign.ML
src/Tools/jEdit/src/token_markup.scala
     1.1 --- a/NEWS	Mon Apr 06 17:28:07 2015 +0200
     1.2 +++ b/NEWS	Mon Apr 06 22:11:01 2015 +0200
     1.3 @@ -6,9 +6,9 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 -* Local theory specifications may have a 'private' modifier to restrict
     1.8 -name space accesses to the current local scope, as delimited by "context
     1.9 -begin ... end". For example, this works like this:
    1.10 +* Local theory specification commands may have a 'private' or
    1.11 +'restricted' modifier to limit name space accesses to the local scope,
    1.12 +as provided by some "context begin ... end" block. For example:
    1.13  
    1.14    context
    1.15    begin
     2.1 --- a/src/Doc/Isar_Ref/Spec.thy	Mon Apr 06 17:28:07 2015 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Mon Apr 06 22:11:01 2015 +0200
     2.3 @@ -115,6 +115,7 @@
     2.4      @{command_def "context"} & : & @{text "theory \<rightarrow> local_theory"} \\
     2.5      @{command_def (local) "end"} & : & @{text "local_theory \<rightarrow> theory"} \\
     2.6      @{keyword_def "private"} \\
     2.7 +    @{keyword_def "restricted"} \\
     2.8    \end{matharray}
     2.9  
    2.10    A local theory target is a specification context that is managed
    2.11 @@ -161,12 +162,16 @@
    2.12    (global) "end"} has a different meaning: it concludes the theory
    2.13    itself (\secref{sec:begin-thy}).
    2.14    
    2.15 -  \item @{keyword "private"} may be given as a modifier to any local theory
    2.16 -  command (before the command keyword). This limits name space accesses to
    2.17 -  the current local scope, as determined by the enclosing @{command
    2.18 -  "context"}~@{keyword "begin"}~\dots~@{command "end"} block. Neither a
    2.19 -  global theory nor a locale target have such a local scope by themselves:
    2.20 -  an extra unnamed context is required to use @{keyword "private"} here.
    2.21 +  \item @{keyword "private"} or @{keyword "restricted"} may be given as
    2.22 +  modifiers before any local theory command. This limits name space accesses
    2.23 +  to the local scope, as determined by the enclosing @{command
    2.24 +  "context"}~@{keyword "begin"}~\dots~@{command "end"} block. Outside its
    2.25 +  scope, a @{keyword "private"} name is inaccessible, and a @{keyword
    2.26 +  "restricted"} name is only accessible with additional qualification.
    2.27 +
    2.28 +  Neither a global @{command theory} nor a @{command locale} target provides
    2.29 +  a local scope by itself: an extra unnamed context is required to use
    2.30 +  @{keyword "private"} or @{keyword "restricted"} here.
    2.31  
    2.32    \item @{text "("}@{keyword_def "in"}~@{text "c)"} given after any local
    2.33    theory command specifies an immediate target, e.g.\ ``@{command
     3.1 --- a/src/Pure/General/binding.ML	Mon Apr 06 17:28:07 2015 +0200
     3.2 +++ b/src/Pure/General/binding.ML	Mon Apr 06 22:11:01 2015 +0200
     3.3 @@ -31,7 +31,8 @@
     3.4    val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding
     3.5    val prefix: bool -> string -> binding -> binding
     3.6    val private: scope -> binding -> binding
     3.7 -  val private_default: scope option -> binding -> binding
     3.8 +  val restricted: scope -> binding -> binding
     3.9 +  val limited_default: (bool * scope) option -> binding -> binding
    3.10    val concealed: binding -> binding
    3.11    val pretty: binding -> Pretty.T
    3.12    val print: binding -> string
    3.13 @@ -39,7 +40,7 @@
    3.14    val bad: binding -> string
    3.15    val check: binding -> unit
    3.16    val name_spec: scope list -> (string * bool) list -> binding ->
    3.17 -    {accessible: bool, concealed: bool, spec: (string * bool) list}
    3.18 +    {limitation: bool option, concealed: bool, spec: (string * bool) list}
    3.19  end;
    3.20  
    3.21  structure Binding: BINDING =
    3.22 @@ -47,7 +48,7 @@
    3.23  
    3.24  (** representation **)
    3.25  
    3.26 -(* scope of private entries *)
    3.27 +(* scope of limited entries *)
    3.28  
    3.29  datatype scope = Scope of serial;
    3.30  
    3.31 @@ -57,19 +58,19 @@
    3.32  (* binding *)
    3.33  
    3.34  datatype binding = Binding of
    3.35 - {private: scope option,            (*entry is strictly private within its scope*)
    3.36 -  concealed: bool,                  (*entry is for foundational purposes -- please ignore*)
    3.37 -  prefix: (string * bool) list,     (*system prefix*)
    3.38 -  qualifier: (string * bool) list,  (*user qualifier*)
    3.39 -  name: bstring,                    (*base name*)
    3.40 -  pos: Position.T};                 (*source position*)
    3.41 + {limited: (bool * scope) option,  (*entry is private (true) / restricted (false) to scope*)
    3.42 +  concealed: bool,                 (*entry is for foundational purposes -- please ignore*)
    3.43 +  prefix: (string * bool) list,    (*system prefix*)
    3.44 +  qualifier: (string * bool) list, (*user qualifier*)
    3.45 +  name: bstring,                   (*base name*)
    3.46 +  pos: Position.T};                (*source position*)
    3.47  
    3.48 -fun make_binding (private, concealed, prefix, qualifier, name, pos) =
    3.49 -  Binding {private = private, concealed = concealed, prefix = prefix,
    3.50 +fun make_binding (limited, concealed, prefix, qualifier, name, pos) =
    3.51 +  Binding {limited = limited, concealed = concealed, prefix = prefix,
    3.52      qualifier = qualifier, name = name, pos = pos};
    3.53  
    3.54 -fun map_binding f (Binding {private, concealed, prefix, qualifier, name, pos}) =
    3.55 -  make_binding (f (private, concealed, prefix, qualifier, name, pos));
    3.56 +fun map_binding f (Binding {limited, concealed, prefix, qualifier, name, pos}) =
    3.57 +  make_binding (f (limited, concealed, prefix, qualifier, name, pos));
    3.58  
    3.59  fun path_of (Binding {prefix, qualifier, ...}) = prefix @ qualifier;
    3.60  
    3.61 @@ -83,8 +84,8 @@
    3.62  
    3.63  fun pos_of (Binding {pos, ...}) = pos;
    3.64  fun set_pos pos =
    3.65 -  map_binding (fn (private, concealed, prefix, qualifier, name, _) =>
    3.66 -    (private, concealed, prefix, qualifier, name, pos));
    3.67 +  map_binding (fn (limited, concealed, prefix, qualifier, name, _) =>
    3.68 +    (limited, concealed, prefix, qualifier, name, pos));
    3.69  
    3.70  fun name name = make (name, Position.none);
    3.71  fun name_of (Binding {name, ...}) = name;
    3.72 @@ -92,8 +93,8 @@
    3.73  fun eq_name (b, b') = name_of b = name_of b';
    3.74  
    3.75  fun map_name f =
    3.76 -  map_binding (fn (private, concealed, prefix, qualifier, name, pos) =>
    3.77 -    (private, concealed, prefix, qualifier, f name, pos));
    3.78 +  map_binding (fn (limited, concealed, prefix, qualifier, name, pos) =>
    3.79 +    (limited, concealed, prefix, qualifier, f name, pos));
    3.80  
    3.81  val prefix_name = map_name o prefix;
    3.82  val suffix_name = map_name o suffix;
    3.83 @@ -106,13 +107,13 @@
    3.84  
    3.85  fun qualify _ "" = I
    3.86    | qualify mandatory qual =
    3.87 -      map_binding (fn (private, concealed, prefix, qualifier, name, pos) =>
    3.88 -        (private, concealed, prefix, (qual, mandatory) :: qualifier, name, pos));
    3.89 +      map_binding (fn (limited, concealed, prefix, qualifier, name, pos) =>
    3.90 +        (limited, concealed, prefix, (qual, mandatory) :: qualifier, name, pos));
    3.91  
    3.92  fun qualified mandatory name' =
    3.93 -  map_binding (fn (private, concealed, prefix, qualifier, name, pos) =>
    3.94 +  map_binding (fn (limited, concealed, prefix, qualifier, name, pos) =>
    3.95      let val qualifier' = if name = "" then qualifier else qualifier @ [(name, mandatory)]
    3.96 -    in (private, concealed, prefix, qualifier', name', pos) end);
    3.97 +    in (limited, concealed, prefix, qualifier', name', pos) end);
    3.98  
    3.99  fun qualified_name "" = empty
   3.100    | qualified_name s =
   3.101 @@ -125,8 +126,8 @@
   3.102  fun prefix_of (Binding {prefix, ...}) = prefix;
   3.103  
   3.104  fun map_prefix f =
   3.105 -  map_binding (fn (private, concealed, prefix, qualifier, name, pos) =>
   3.106 -    (private, concealed, f prefix, qualifier, name, pos));
   3.107 +  map_binding (fn (limited, concealed, prefix, qualifier, name, pos) =>
   3.108 +    (limited, concealed, f prefix, qualifier, name, pos));
   3.109  
   3.110  fun prefix _ "" = I
   3.111    | prefix mandatory prfx = map_prefix (cons (prfx, mandatory));
   3.112 @@ -134,17 +135,20 @@
   3.113  
   3.114  (* visibility flags *)
   3.115  
   3.116 -fun private scope =
   3.117 +fun limited strict scope =
   3.118    map_binding (fn (_, concealed, prefix, qualifier, name, pos) =>
   3.119 -    (SOME scope, concealed, prefix, qualifier, name, pos));
   3.120 +    (SOME (strict, scope), concealed, prefix, qualifier, name, pos));
   3.121  
   3.122 -fun private_default private' =
   3.123 -  map_binding (fn (private, concealed, prefix, qualifier, name, pos) =>
   3.124 -    (if is_some private then private else private', concealed, prefix, qualifier, name, pos));
   3.125 +val private = limited true;
   3.126 +val restricted = limited false;
   3.127 +
   3.128 +fun limited_default limited' =
   3.129 +  map_binding (fn (limited, concealed, prefix, qualifier, name, pos) =>
   3.130 +    (if is_some limited then limited else limited', concealed, prefix, qualifier, name, pos));
   3.131  
   3.132  val concealed =
   3.133 -  map_binding (fn (private, _, prefix, qualifier, name, pos) =>
   3.134 -    (private, true, prefix, qualifier, name, pos));
   3.135 +  map_binding (fn (limited, _, prefix, qualifier, name, pos) =>
   3.136 +    (limited, true, prefix, qualifier, name, pos));
   3.137  
   3.138  
   3.139  (* print *)
   3.140 @@ -177,13 +181,13 @@
   3.141  
   3.142  fun name_spec scopes path binding =
   3.143    let
   3.144 -    val Binding {private, concealed, prefix, qualifier, name, ...} = binding;
   3.145 +    val Binding {limited, concealed, prefix, qualifier, name, ...} = binding;
   3.146      val _ = Long_Name.is_qualified name andalso error (bad binding);
   3.147  
   3.148 -    val accessible =
   3.149 -      (case private of
   3.150 -        NONE => true
   3.151 -      | SOME scope => member (op =) scopes scope);
   3.152 +    val limitation =
   3.153 +      (case limited of
   3.154 +        NONE => NONE
   3.155 +      | SOME (strict, scope) => if member (op =) scopes scope then NONE else SOME strict);
   3.156  
   3.157      val spec1 =
   3.158        maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path @ prefix @ qualifier);
   3.159 @@ -192,7 +196,7 @@
   3.160      val _ =
   3.161        exists (fn (a, _) => member (op =) bad_specs a orelse exists_string (fn s => s = "\"") a) spec
   3.162        andalso error (bad binding);
   3.163 -  in {accessible = accessible, concealed = concealed, spec = if null spec2 then [] else spec} end;
   3.164 +  in {limitation = limitation, concealed = concealed, spec = if null spec2 then [] else spec} end;
   3.165  
   3.166  end;
   3.167  
     4.1 --- a/src/Pure/General/name_space.ML	Mon Apr 06 17:28:07 2015 +0200
     4.2 +++ b/src/Pure/General/name_space.ML	Mon Apr 06 22:11:01 2015 +0200
     4.3 @@ -35,8 +35,11 @@
     4.4    val get_scopes: naming -> Binding.scope list
     4.5    val get_scope: naming -> Binding.scope option
     4.6    val new_scope: naming -> Binding.scope * naming
     4.7 +  val limited: bool -> Position.T -> naming -> naming
     4.8    val private_scope: Binding.scope -> naming -> naming
     4.9    val private: Position.T -> naming -> naming
    4.10 +  val restricted_scope: Binding.scope -> naming -> naming
    4.11 +  val restricted: Position.T -> naming -> naming
    4.12    val concealed: naming -> naming
    4.13    val get_group: naming -> serial option
    4.14    val set_group: serial option -> naming -> naming
    4.15 @@ -297,62 +300,73 @@
    4.16  
    4.17  datatype naming = Naming of
    4.18   {scopes: Binding.scope list,
    4.19 -  private: Binding.scope option,
    4.20 +  limited: (bool * Binding.scope) option,
    4.21    concealed: bool,
    4.22    group: serial option,
    4.23    theory_name: string,
    4.24    path: (string * bool) list};
    4.25  
    4.26 -fun make_naming (scopes, private, concealed, group, theory_name, path) =
    4.27 -  Naming {scopes = scopes, private = private, concealed = concealed,
    4.28 +fun make_naming (scopes, limited, concealed, group, theory_name, path) =
    4.29 +  Naming {scopes = scopes, limited = limited, concealed = concealed,
    4.30      group = group, theory_name = theory_name, path = path};
    4.31  
    4.32 -fun map_naming f (Naming {scopes, private, concealed, group, theory_name, path}) =
    4.33 -  make_naming (f (scopes, private, concealed, group, theory_name, path));
    4.34 +fun map_naming f (Naming {scopes, limited, concealed, group, theory_name, path}) =
    4.35 +  make_naming (f (scopes, limited, concealed, group, theory_name, path));
    4.36  
    4.37 -fun map_path f = map_naming (fn (scopes, private, concealed, group, theory_name, path) =>
    4.38 -  (scopes, private, concealed, group, theory_name, f path));
    4.39  
    4.40 +(* scope and access limitation *)
    4.41  
    4.42  fun get_scopes (Naming {scopes, ...}) = scopes;
    4.43  val get_scope = try hd o get_scopes;
    4.44  
    4.45 -fun put_scope scope =
    4.46 -  map_naming (fn (scopes, private, concealed, group, theory_name, path) =>
    4.47 -    (scope :: scopes, private, concealed, group, theory_name, path));
    4.48 -
    4.49  fun new_scope naming =
    4.50    let
    4.51      val scope = Binding.new_scope ();
    4.52      val naming' =
    4.53 -      naming |> map_naming (fn (scopes, private, concealed, group, theory_name, path) =>
    4.54 -        (scope :: scopes, private, concealed, group, theory_name, path));
    4.55 +      naming |> map_naming (fn (scopes, limited, concealed, group, theory_name, path) =>
    4.56 +        (scope :: scopes, limited, concealed, group, theory_name, path));
    4.57    in (scope, naming') end;
    4.58  
    4.59 -fun private_scope scope = map_naming (fn (scopes, _, concealed, group, theory_name, path) =>
    4.60 -  (scopes, SOME scope, concealed, group, theory_name, path));
    4.61 +fun limited_scope strict scope =
    4.62 +  map_naming (fn (scopes, _, concealed, group, theory_name, path) =>
    4.63 +    (scopes, SOME (strict, scope), concealed, group, theory_name, path));
    4.64  
    4.65 -fun private pos naming =
    4.66 +fun limited strict pos naming =
    4.67    (case get_scope naming of
    4.68 -    SOME scope => private_scope scope naming
    4.69 -  | NONE => error ("Missing local scope -- cannot declare private names" ^ Position.here pos));
    4.70 +    SOME scope => limited_scope strict scope naming
    4.71 +  | NONE => error ("Missing local scope -- cannot limit name space accesses" ^ Position.here pos));
    4.72 +
    4.73 +val private_scope = limited_scope true;
    4.74 +val private = limited true;
    4.75 +
    4.76 +val restricted_scope = limited_scope false;
    4.77 +val restricted = limited false;
    4.78  
    4.79 -val concealed = map_naming (fn (scopes, private, _, group, theory_name, path) =>
    4.80 -  (scopes, private, true, group, theory_name, path));
    4.81 +val concealed = map_naming (fn (scopes, limited, _, group, theory_name, path) =>
    4.82 +  (scopes, limited, true, group, theory_name, path));
    4.83 +
    4.84  
    4.85 -fun set_theory_name theory_name = map_naming (fn (scopes, private, concealed, group, _, path) =>
    4.86 -  (scopes, private, concealed, group, theory_name, path));
    4.87 +(* additional structural info *)
    4.88 +
    4.89 +fun set_theory_name theory_name = map_naming (fn (scopes, limited, concealed, group, _, path) =>
    4.90 +  (scopes, limited, concealed, group, theory_name, path));
    4.91  
    4.92  fun get_group (Naming {group, ...}) = group;
    4.93  
    4.94 -fun set_group group = map_naming (fn (scopes, private, concealed, _, theory_name, path) =>
    4.95 -  (scopes, private, concealed, group, theory_name, path));
    4.96 +fun set_group group = map_naming (fn (scopes, limited, concealed, _, theory_name, path) =>
    4.97 +  (scopes, limited, concealed, group, theory_name, path));
    4.98  
    4.99  fun new_group naming = set_group (SOME (serial ())) naming;
   4.100  val reset_group = set_group NONE;
   4.101  
   4.102 +
   4.103 +(* name entry path *)
   4.104 +
   4.105  fun get_path (Naming {path, ...}) = path;
   4.106  
   4.107 +fun map_path f = map_naming (fn (scopes, limited, concealed, group, theory_name, path) =>
   4.108 +  (scopes, limited, concealed, group, theory_name, f path));
   4.109 +
   4.110  fun add_path elems = map_path (fn path => path @ [(elems, false)]);
   4.111  val root_path = map_path (fn _ => []);
   4.112  val parent_path = map_path (perhaps (try (#1 o split_last)));
   4.113 @@ -365,14 +379,16 @@
   4.114  val local_naming = global_naming |> add_path Long_Name.localN;
   4.115  
   4.116  
   4.117 -(* visibility flags *)
   4.118 +(* transform *)
   4.119  
   4.120 -fun transform_naming (Naming {private = private', concealed = concealed', ...}) =
   4.121 -  fold private_scope (the_list private') #>
   4.122 +fun transform_naming (Naming {limited = limited', concealed = concealed', ...}) =
   4.123 +  (case limited' of
   4.124 +    SOME (strict, scope) => limited_scope strict scope
   4.125 +  | NONE => I) #>
   4.126    concealed' ? concealed;
   4.127  
   4.128 -fun transform_binding (Naming {private, concealed, ...}) =
   4.129 -  Binding.private_default private #>
   4.130 +fun transform_binding (Naming {limited, concealed, ...}) =
   4.131 +  Binding.limited_default limited #>
   4.132    concealed ? Binding.concealed;
   4.133  
   4.134  
   4.135 @@ -400,11 +416,12 @@
   4.136  
   4.137  fun accesses naming binding =
   4.138    (case name_spec naming binding of
   4.139 -    {accessible = false, ...} => ([], [])
   4.140 -  | {spec, ...} =>
   4.141 +    {limitation = SOME true, ...} => ([], [])
   4.142 +  | {limitation, spec, ...} =>
   4.143        let
   4.144 -        val sfxs = mandatory_suffixes spec;
   4.145 -        val pfxs = mandatory_prefixes spec;
   4.146 +        val restrict = is_some limitation ? filter (fn [_] => false | _ => true);
   4.147 +        val sfxs = restrict (mandatory_suffixes spec);
   4.148 +        val pfxs = restrict (mandatory_prefixes spec);
   4.149        in apply2 (map Long_Name.implode) (sfxs @ pfxs, sfxs) end);
   4.150  
   4.151  
     5.1 --- a/src/Pure/Isar/outer_syntax.ML	Mon Apr 06 17:28:07 2015 +0200
     5.2 +++ b/src/Pure/Isar/outer_syntax.ML	Mon Apr 06 22:11:01 2015 +0200
     5.3 @@ -44,7 +44,8 @@
     5.4  
     5.5  datatype command_parser =
     5.6    Parser of (Toplevel.transition -> Toplevel.transition) parser |
     5.7 -  Private_Parser of Position.T option -> (Toplevel.transition -> Toplevel.transition) parser;
     5.8 +  Limited_Parser of
     5.9 +    (bool * Position.T) option -> (Toplevel.transition -> Toplevel.transition) parser;
    5.10  
    5.11  datatype command = Command of
    5.12   {comment: string,
    5.13 @@ -145,8 +146,8 @@
    5.14  
    5.15  fun local_theory_command trans command_keyword comment parse =
    5.16    raw_command command_keyword comment
    5.17 -    (Private_Parser (fn private =>
    5.18 -      Parse.opt_target -- parse >> (fn (target, f) => trans private target f)));
    5.19 +    (Limited_Parser (fn limited =>
    5.20 +      Parse.opt_target -- parse >> (fn (target, f) => trans limited target f)));
    5.21  
    5.22  val local_theory' = local_theory_command Toplevel.local_theory';
    5.23  val local_theory = local_theory_command Toplevel.local_theory;
    5.24 @@ -161,8 +162,11 @@
    5.25  
    5.26  local
    5.27  
    5.28 +val before_command =
    5.29 +  Scan.option (Parse.position (Parse.private >> K true || Parse.restricted >> K false));
    5.30 +
    5.31  fun parse_command thy =
    5.32 -  Scan.ahead (Parse.opt_private |-- Parse.position Parse.command_) :|-- (fn (name, pos) =>
    5.33 +  Scan.ahead (before_command |-- Parse.position Parse.command_) :|-- (fn (name, pos) =>
    5.34      let
    5.35        val command_tags = Parse.command_ -- Parse.tags;
    5.36        val tr0 = Toplevel.empty |> Toplevel.name name |> Toplevel.position pos;
    5.37 @@ -170,9 +174,9 @@
    5.38        (case lookup_commands thy name of
    5.39          SOME (Command {command_parser = Parser parse, ...}) =>
    5.40            Parse.!!! (command_tags |-- parse) >> (fn f => f tr0)
    5.41 -      | SOME (Command {command_parser = Private_Parser parse, ...}) =>
    5.42 -          Parse.opt_private :|-- (fn private =>
    5.43 -            Parse.!!! (command_tags |-- parse private)) >> (fn f => f tr0)
    5.44 +      | SOME (Command {command_parser = Limited_Parser parse, ...}) =>
    5.45 +          before_command :|-- (fn limited =>
    5.46 +            Parse.!!! (command_tags |-- parse limited)) >> (fn f => f tr0)
    5.47        | NONE =>
    5.48            Scan.succeed
    5.49              (tr0 |> Toplevel.imperative (fn () => err_command "Undefined command " name [pos])))
    5.50 @@ -225,9 +229,9 @@
    5.51  
    5.52  fun parse tok (result, content, improper) =
    5.53    if Token.is_improper tok then (result, content, tok :: improper)
    5.54 -  else if Token.is_private tok orelse
    5.55 +  else if Token.is_command_modifier tok orelse
    5.56      Token.is_command tok andalso
    5.57 -      (not (exists Token.is_private content) orelse exists Token.is_command content)
    5.58 +      (not (exists Token.is_command_modifier content) orelse exists Token.is_command content)
    5.59    then (flush (result, content, improper), [tok], [])
    5.60    else (result, tok :: (improper @ content), []);
    5.61  
     6.1 --- a/src/Pure/Isar/outer_syntax.scala	Mon Apr 06 17:28:07 2015 +0200
     6.2 +++ b/src/Pure/Isar/outer_syntax.scala	Mon Apr 06 22:11:01 2015 +0200
     6.3 @@ -219,8 +219,8 @@
     6.4  
     6.5      for (tok <- toks) {
     6.6        if (tok.is_improper) improper += tok
     6.7 -      else if (tok.is_private ||
     6.8 -        tok.is_command && (!content.exists(_.is_private) || content.exists(_.is_command)))
     6.9 +      else if (tok.is_command_modifier ||
    6.10 +        tok.is_command && (!content.exists(_.is_command_modifier) || content.exists(_.is_command)))
    6.11        { flush(); content += tok }
    6.12        else { content ++= improper; improper.clear; content += tok }
    6.13      }
     7.1 --- a/src/Pure/Isar/parse.ML	Mon Apr 06 17:28:07 2015 +0200
     7.2 +++ b/src/Pure/Isar/parse.ML	Mon Apr 06 22:11:01 2015 +0200
     7.3 @@ -104,7 +104,7 @@
     7.4    val propp: (string * string list) parser
     7.5    val termp: (string * string list) parser
     7.6    val private: Position.T parser
     7.7 -  val opt_private: Position.T option parser
     7.8 +  val restricted: Position.T parser
     7.9    val target: (xstring * Position.T) parser
    7.10    val opt_target: (xstring * Position.T) option parser
    7.11    val args: Token.T list parser
    7.12 @@ -401,7 +401,7 @@
    7.13  (* target information *)
    7.14  
    7.15  val private = position ($$$ "private") >> #2;
    7.16 -val opt_private = Scan.option private;
    7.17 +val restricted = position ($$$ "restricted") >> #2;
    7.18  
    7.19  val target = ($$$ "(" -- $$$ "in") |-- !!! (position xname --| $$$ ")");
    7.20  val opt_target = Scan.option target;
     8.1 --- a/src/Pure/Isar/proof_context.ML	Mon Apr 06 17:28:07 2015 +0200
     8.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Apr 06 22:11:01 2015 +0200
     8.3 @@ -38,6 +38,8 @@
     8.4    val new_scope: Proof.context -> Binding.scope * Proof.context
     8.5    val private_scope: Binding.scope -> Proof.context -> Proof.context
     8.6    val private: Position.T -> Proof.context -> Proof.context
     8.7 +  val restricted_scope: Binding.scope -> Proof.context -> Proof.context
     8.8 +  val restricted: Position.T -> Proof.context -> Proof.context
     8.9    val concealed: Proof.context -> Proof.context
    8.10    val class_space: Proof.context -> Name_Space.T
    8.11    val type_space: Proof.context -> Name_Space.T
    8.12 @@ -319,6 +321,9 @@
    8.13  
    8.14  val private_scope = map_naming o Name_Space.private_scope;
    8.15  val private = map_naming o Name_Space.private;
    8.16 +val restricted_scope = map_naming o Name_Space.restricted_scope;
    8.17 +val restricted = map_naming o Name_Space.restricted;
    8.18 +
    8.19  val concealed = map_naming Name_Space.concealed;
    8.20  
    8.21  
     9.1 --- a/src/Pure/Isar/token.ML	Mon Apr 06 17:28:07 2015 +0200
     9.2 +++ b/src/Pure/Isar/token.ML	Mon Apr 06 22:11:01 2015 +0200
     9.3 @@ -46,7 +46,7 @@
     9.4    val is_command: T -> bool
     9.5    val is_name: T -> bool
     9.6    val keyword_with: (string -> bool) -> T -> bool
     9.7 -  val is_private: T -> bool
     9.8 +  val is_command_modifier: T -> bool
     9.9    val ident_with: (string -> bool) -> T -> bool
    9.10    val is_proper: T -> bool
    9.11    val is_improper: T -> bool
    9.12 @@ -247,7 +247,7 @@
    9.13  fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x
    9.14    | keyword_with _ _ = false;
    9.15  
    9.16 -val is_private = keyword_with (fn x => x = "private");
    9.17 +val is_command_modifier = keyword_with (fn x => x = "private" orelse x = "restricted");
    9.18  
    9.19  fun ident_with pred (Token (_, (Ident, x), _)) = pred x
    9.20    | ident_with _ _ = false;
    10.1 --- a/src/Pure/Isar/token.scala	Mon Apr 06 17:28:07 2015 +0200
    10.2 +++ b/src/Pure/Isar/token.scala	Mon Apr 06 22:11:01 2015 +0200
    10.3 @@ -259,7 +259,8 @@
    10.4    def is_begin: Boolean = is_keyword && source == "begin"
    10.5    def is_end: Boolean = is_command && source == "end"
    10.6  
    10.7 -  def is_private: Boolean = is_keyword && source == "private"
    10.8 +  def is_command_modifier: Boolean =
    10.9 +    is_keyword && (source == "private" || source == "restricted")
   10.10  
   10.11    def is_begin_block: Boolean = is_command && source == "{"
   10.12    def is_end_block: Boolean = is_command && source == "}"
    11.1 --- a/src/Pure/Isar/toplevel.ML	Mon Apr 06 17:28:07 2015 +0200
    11.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Apr 06 22:11:01 2015 +0200
    11.3 @@ -51,15 +51,15 @@
    11.4    val end_local_theory: transition -> transition
    11.5    val open_target: (generic_theory -> local_theory) -> transition -> transition
    11.6    val close_target: transition -> transition
    11.7 -  val local_theory': Position.T option -> (xstring * Position.T) option ->
    11.8 +  val local_theory': (bool * Position.T) option -> (xstring * Position.T) option ->
    11.9      (bool -> local_theory -> local_theory) -> transition -> transition
   11.10 -  val local_theory: Position.T option -> (xstring * Position.T) option ->
   11.11 +  val local_theory: (bool * Position.T) option -> (xstring * Position.T) option ->
   11.12      (local_theory -> local_theory) -> transition -> transition
   11.13    val present_local_theory: (xstring * Position.T) option -> (state -> unit) ->
   11.14      transition -> transition
   11.15 -  val local_theory_to_proof': Position.T option -> (xstring * Position.T) option ->
   11.16 +  val local_theory_to_proof': (bool * Position.T) option -> (xstring * Position.T) option ->
   11.17      (bool -> local_theory -> Proof.state) -> transition -> transition
   11.18 -  val local_theory_to_proof: Position.T option -> (xstring * Position.T) option ->
   11.19 +  val local_theory_to_proof: (bool * Position.T) option -> (xstring * Position.T) option ->
   11.20      (local_theory -> Proof.state) -> transition -> transition
   11.21    val theory_to_proof: (theory -> Proof.state) -> transition -> transition
   11.22    val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition
   11.23 @@ -412,12 +412,15 @@
   11.24          | NONE => raise UNDEF)
   11.25      | _ => raise UNDEF));
   11.26  
   11.27 -fun local_theory' private target f = present_transaction (fn int =>
   11.28 +val limited_context =
   11.29 +  fn SOME (strict, scope) => Proof_Context.map_naming (Name_Space.limited strict scope) | NONE => I;
   11.30 +
   11.31 +fun local_theory' limited target f = present_transaction (fn int =>
   11.32    (fn Theory (gthy, _) =>
   11.33          let
   11.34            val (finish, lthy) = Named_Target.switch target gthy;
   11.35            val lthy' = lthy
   11.36 -            |> fold Proof_Context.private (the_list private)
   11.37 +            |> limited_context limited
   11.38              |> Local_Theory.new_group
   11.39              |> f int
   11.40              |> Local_Theory.reset_group;
   11.41 @@ -425,7 +428,7 @@
   11.42      | _ => raise UNDEF))
   11.43    (K ());
   11.44  
   11.45 -fun local_theory private target f = local_theory' private target (K f);
   11.46 +fun local_theory limited target f = local_theory' limited target (K f);
   11.47  
   11.48  fun present_local_theory target = present_transaction (fn int =>
   11.49    (fn Theory (gthy, _) =>
   11.50 @@ -470,18 +473,18 @@
   11.51  
   11.52  in
   11.53  
   11.54 -fun local_theory_to_proof' private target f = begin_proof
   11.55 +fun local_theory_to_proof' limited target f = begin_proof
   11.56    (fn int => fn gthy =>
   11.57      let
   11.58        val (finish, lthy) = Named_Target.switch target gthy;
   11.59        val prf = lthy
   11.60 -        |> fold Proof_Context.private (the_list private)
   11.61 +        |> limited_context limited
   11.62          |> Local_Theory.new_group
   11.63          |> f int;
   11.64      in (finish o Local_Theory.reset_group, prf) end);
   11.65  
   11.66 -fun local_theory_to_proof private target f =
   11.67 -  local_theory_to_proof' private target (K f);
   11.68 +fun local_theory_to_proof limited target f =
   11.69 +  local_theory_to_proof' limited target (K f);
   11.70  
   11.71  fun theory_to_proof f = begin_proof
   11.72    (fn _ => fn gthy =>
    12.1 --- a/src/Pure/Pure.thy	Mon Apr 06 17:28:07 2015 +0200
    12.2 +++ b/src/Pure/Pure.thy	Mon Apr 06 22:11:01 2015 +0200
    12.3 @@ -11,8 +11,8 @@
    12.4      "\<subseteq>" "]" "assumes" "attach" "binder" "constrains"
    12.5      "defines" "fixes" "for" "identifier" "if" "in" "includes" "infix"
    12.6      "infixl" "infixr" "is" "notes" "obtains" "open" "output"
    12.7 -    "overloaded" "pervasive" "private" "shows" "structure" "unchecked"
    12.8 -    "where" "|"
    12.9 +    "overloaded" "pervasive" "private" "restricted" "shows"
   12.10 +    "structure" "unchecked" "where" "|"
   12.11    and "text" "txt" :: document_body
   12.12    and "text_raw" :: document_raw
   12.13    and "default_sort" :: thy_decl == ""
    13.1 --- a/src/Pure/Thy/thy_output.ML	Mon Apr 06 17:28:07 2015 +0200
    13.2 +++ b/src/Pure/Thy/thy_output.ML	Mon Apr 06 22:11:01 2015 +0200
    13.3 @@ -384,10 +384,10 @@
    13.4          in (SOME (name, pos', tags), (mk (name, source), (flag, d))) end));
    13.5  
    13.6      val command = Scan.peek (fn d =>
    13.7 -      Scan.optional (Scan.one Token.is_private -- improper >> op ::) [] --
    13.8 +      Scan.optional (Scan.one Token.is_command_modifier -- improper >> op ::) [] --
    13.9        Scan.one Token.is_command -- Scan.repeat tag
   13.10 -      >> (fn ((private, cmd), tags) =>
   13.11 -        map (fn tok => (NONE, (Basic_Token tok, ("", d)))) private @
   13.12 +      >> (fn ((cmd_mod, cmd), tags) =>
   13.13 +        map (fn tok => (NONE, (Basic_Token tok, ("", d)))) cmd_mod @
   13.14            [(SOME (Token.content_of cmd, Token.pos_of cmd, tags),
   13.15              (Basic_Token cmd, (Latex.markup_false, d)))]));
   13.16  
    14.1 --- a/src/Pure/sign.ML	Mon Apr 06 17:28:07 2015 +0200
    14.2 +++ b/src/Pure/sign.ML	Mon Apr 06 22:11:01 2015 +0200
    14.3 @@ -525,6 +525,8 @@
    14.4  
    14.5  val private_scope = map_naming o Name_Space.private_scope;
    14.6  val private = map_naming o Name_Space.private;
    14.7 +val restricted_scope = map_naming o Name_Space.restricted_scope;
    14.8 +val restricted = map_naming o Name_Space.restricted;
    14.9  val concealed = map_naming Name_Space.concealed;
   14.10  
   14.11  
    15.1 --- a/src/Tools/jEdit/src/token_markup.scala	Mon Apr 06 17:28:07 2015 +0200
    15.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Mon Apr 06 22:11:01 2015 +0200
    15.3 @@ -274,11 +274,11 @@
    15.4    {
    15.5      def maybe_command_start(i: Text.Offset): Option[Text.Info[Token]] =
    15.6        token_reverse_iterator(syntax, buffer, i).
    15.7 -        find(info => info.info.is_private || info.info.is_command)
    15.8 +        find(info => info.info.is_command_modifier || info.info.is_command)
    15.9  
   15.10      def maybe_command_stop(i: Text.Offset): Option[Text.Info[Token]] =
   15.11        token_iterator(syntax, buffer, i).
   15.12 -        find(info => info.info.is_private || info.info.is_command)
   15.13 +        find(info => info.info.is_command_modifier || info.info.is_command)
   15.14  
   15.15      if (JEdit_Lib.buffer_range(buffer).contains(offset)) {
   15.16        val start_info =
   15.17 @@ -288,15 +288,15 @@
   15.18            case Some(Text.Info(range1, tok1)) if tok1.is_command =>
   15.19              val info2 = maybe_command_start(range1.start - 1)
   15.20              info2 match {
   15.21 -              case Some(Text.Info(_, tok2)) if tok2.is_private => info2
   15.22 +              case Some(Text.Info(_, tok2)) if tok2.is_command_modifier => info2
   15.23                case _ => info1
   15.24              }
   15.25            case _ => info1
   15.26          }
   15.27        }
   15.28 -      val (start_is_private, start, start_next) =
   15.29 +      val (start_is_command_modifier, start, start_next) =
   15.30          start_info match {
   15.31 -          case Some(Text.Info(range, tok)) => (tok.is_private, range.start, range.stop)
   15.32 +          case Some(Text.Info(range, tok)) => (tok.is_command_modifier, range.start, range.stop)
   15.33            case None => (false, 0, 0)
   15.34          }
   15.35  
   15.36 @@ -304,7 +304,7 @@
   15.37        {
   15.38          val info1 = maybe_command_stop(start_next)
   15.39          info1 match {
   15.40 -          case Some(Text.Info(range1, tok1)) if tok1.is_command && start_is_private =>
   15.41 +          case Some(Text.Info(range1, tok1)) if tok1.is_command && start_is_command_modifier =>
   15.42              maybe_command_stop(range1.stop)
   15.43            case _ => info1
   15.44          }