# HG changeset patch
# User wenzelm
# Date 1428351061 -7200
# Node ID 7d46aa03696e6b8ad8aec0acc08f24da743fa920
# Parent  f84b93187ab62d57b0ca4a60f6d7a58be4d7ba4c
support for 'restricted' modifier: only qualified accesses outside the local scope;

diff -r f84b93187ab6 -r 7d46aa03696e NEWS
--- a/NEWS	Mon Apr 06 17:28:07 2015 +0200
+++ b/NEWS	Mon Apr 06 22:11:01 2015 +0200
@@ -6,9 +6,9 @@
 
 *** General ***
 
-* Local theory specifications may have a 'private' modifier to restrict
-name space accesses to the current local scope, as delimited by "context
-begin ... end". For example, this works like this:
+* Local theory specification commands may have a 'private' or
+'restricted' modifier to limit name space accesses to the local scope,
+as provided by some "context begin ... end" block. For example:
 
   context
   begin
diff -r f84b93187ab6 -r 7d46aa03696e src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Mon Apr 06 17:28:07 2015 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Mon Apr 06 22:11:01 2015 +0200
@@ -115,6 +115,7 @@
     @{command_def "context"} & : & @{text "theory \<rightarrow> local_theory"} \\
     @{command_def (local) "end"} & : & @{text "local_theory \<rightarrow> theory"} \\
     @{keyword_def "private"} \\
+    @{keyword_def "restricted"} \\
   \end{matharray}
 
   A local theory target is a specification context that is managed
@@ -161,12 +162,16 @@
   (global) "end"} has a different meaning: it concludes the theory
   itself (\secref{sec:begin-thy}).
   
-  \item @{keyword "private"} may be given as a modifier to any local theory
-  command (before the command keyword). This limits name space accesses to
-  the current local scope, as determined by the enclosing @{command
-  "context"}~@{keyword "begin"}~\dots~@{command "end"} block. Neither a
-  global theory nor a locale target have such a local scope by themselves:
-  an extra unnamed context is required to use @{keyword "private"} here.
+  \item @{keyword "private"} or @{keyword "restricted"} may be given as
+  modifiers before any local theory command. This limits name space accesses
+  to the local scope, as determined by the enclosing @{command
+  "context"}~@{keyword "begin"}~\dots~@{command "end"} block. Outside its
+  scope, a @{keyword "private"} name is inaccessible, and a @{keyword
+  "restricted"} name is only accessible with additional qualification.
+
+  Neither a global @{command theory} nor a @{command locale} target provides
+  a local scope by itself: an extra unnamed context is required to use
+  @{keyword "private"} or @{keyword "restricted"} here.
 
   \item @{text "("}@{keyword_def "in"}~@{text "c)"} given after any local
   theory command specifies an immediate target, e.g.\ ``@{command
diff -r f84b93187ab6 -r 7d46aa03696e src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Mon Apr 06 17:28:07 2015 +0200
+++ b/src/Pure/General/binding.ML	Mon Apr 06 22:11:01 2015 +0200
@@ -31,7 +31,8 @@
   val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding
   val prefix: bool -> string -> binding -> binding
   val private: scope -> binding -> binding
-  val private_default: scope option -> binding -> binding
+  val restricted: scope -> binding -> binding
+  val limited_default: (bool * scope) option -> binding -> binding
   val concealed: binding -> binding
   val pretty: binding -> Pretty.T
   val print: binding -> string
@@ -39,7 +40,7 @@
   val bad: binding -> string
   val check: binding -> unit
   val name_spec: scope list -> (string * bool) list -> binding ->
-    {accessible: bool, concealed: bool, spec: (string * bool) list}
+    {limitation: bool option, concealed: bool, spec: (string * bool) list}
 end;
 
 structure Binding: BINDING =
@@ -47,7 +48,7 @@
 
 (** representation **)
 
-(* scope of private entries *)
+(* scope of limited entries *)
 
 datatype scope = Scope of serial;
 
@@ -57,19 +58,19 @@
 (* binding *)
 
 datatype binding = Binding of
- {private: scope option,            (*entry is strictly private within its scope*)
-  concealed: bool,                  (*entry is for foundational purposes -- please ignore*)
-  prefix: (string * bool) list,     (*system prefix*)
-  qualifier: (string * bool) list,  (*user qualifier*)
-  name: bstring,                    (*base name*)
-  pos: Position.T};                 (*source position*)
+ {limited: (bool * scope) option,  (*entry is private (true) / restricted (false) to scope*)
+  concealed: bool,                 (*entry is for foundational purposes -- please ignore*)
+  prefix: (string * bool) list,    (*system prefix*)
+  qualifier: (string * bool) list, (*user qualifier*)
+  name: bstring,                   (*base name*)
+  pos: Position.T};                (*source position*)
 
-fun make_binding (private, concealed, prefix, qualifier, name, pos) =
-  Binding {private = private, concealed = concealed, prefix = prefix,
+fun make_binding (limited, concealed, prefix, qualifier, name, pos) =
+  Binding {limited = limited, concealed = concealed, prefix = prefix,
     qualifier = qualifier, name = name, pos = pos};
 
-fun map_binding f (Binding {private, concealed, prefix, qualifier, name, pos}) =
-  make_binding (f (private, concealed, prefix, qualifier, name, pos));
+fun map_binding f (Binding {limited, concealed, prefix, qualifier, name, pos}) =
+  make_binding (f (limited, concealed, prefix, qualifier, name, pos));
 
 fun path_of (Binding {prefix, qualifier, ...}) = prefix @ qualifier;
 
@@ -83,8 +84,8 @@
 
 fun pos_of (Binding {pos, ...}) = pos;
 fun set_pos pos =
-  map_binding (fn (private, concealed, prefix, qualifier, name, _) =>
-    (private, concealed, prefix, qualifier, name, pos));
+  map_binding (fn (limited, concealed, prefix, qualifier, name, _) =>
+    (limited, concealed, prefix, qualifier, name, pos));
 
 fun name name = make (name, Position.none);
 fun name_of (Binding {name, ...}) = name;
@@ -92,8 +93,8 @@
 fun eq_name (b, b') = name_of b = name_of b';
 
 fun map_name f =
-  map_binding (fn (private, concealed, prefix, qualifier, name, pos) =>
-    (private, concealed, prefix, qualifier, f name, pos));
+  map_binding (fn (limited, concealed, prefix, qualifier, name, pos) =>
+    (limited, concealed, prefix, qualifier, f name, pos));
 
 val prefix_name = map_name o prefix;
 val suffix_name = map_name o suffix;
@@ -106,13 +107,13 @@
 
 fun qualify _ "" = I
   | qualify mandatory qual =
-      map_binding (fn (private, concealed, prefix, qualifier, name, pos) =>
-        (private, concealed, prefix, (qual, mandatory) :: qualifier, name, pos));
+      map_binding (fn (limited, concealed, prefix, qualifier, name, pos) =>
+        (limited, concealed, prefix, (qual, mandatory) :: qualifier, name, pos));
 
 fun qualified mandatory name' =
-  map_binding (fn (private, concealed, prefix, qualifier, name, pos) =>
+  map_binding (fn (limited, concealed, prefix, qualifier, name, pos) =>
     let val qualifier' = if name = "" then qualifier else qualifier @ [(name, mandatory)]
-    in (private, concealed, prefix, qualifier', name', pos) end);
+    in (limited, concealed, prefix, qualifier', name', pos) end);
 
 fun qualified_name "" = empty
   | qualified_name s =
@@ -125,8 +126,8 @@
 fun prefix_of (Binding {prefix, ...}) = prefix;
 
 fun map_prefix f =
-  map_binding (fn (private, concealed, prefix, qualifier, name, pos) =>
-    (private, concealed, f prefix, qualifier, name, pos));
+  map_binding (fn (limited, concealed, prefix, qualifier, name, pos) =>
+    (limited, concealed, f prefix, qualifier, name, pos));
 
 fun prefix _ "" = I
   | prefix mandatory prfx = map_prefix (cons (prfx, mandatory));
@@ -134,17 +135,20 @@
 
 (* visibility flags *)
 
-fun private scope =
+fun limited strict scope =
   map_binding (fn (_, concealed, prefix, qualifier, name, pos) =>
-    (SOME scope, concealed, prefix, qualifier, name, pos));
+    (SOME (strict, scope), concealed, prefix, qualifier, name, pos));
 
-fun private_default private' =
-  map_binding (fn (private, concealed, prefix, qualifier, name, pos) =>
-    (if is_some private then private else private', concealed, prefix, qualifier, name, pos));
+val private = limited true;
+val restricted = limited false;
+
+fun limited_default limited' =
+  map_binding (fn (limited, concealed, prefix, qualifier, name, pos) =>
+    (if is_some limited then limited else limited', concealed, prefix, qualifier, name, pos));
 
 val concealed =
-  map_binding (fn (private, _, prefix, qualifier, name, pos) =>
-    (private, true, prefix, qualifier, name, pos));
+  map_binding (fn (limited, _, prefix, qualifier, name, pos) =>
+    (limited, true, prefix, qualifier, name, pos));
 
 
 (* print *)
@@ -177,13 +181,13 @@
 
 fun name_spec scopes path binding =
   let
-    val Binding {private, concealed, prefix, qualifier, name, ...} = binding;
+    val Binding {limited, concealed, prefix, qualifier, name, ...} = binding;
     val _ = Long_Name.is_qualified name andalso error (bad binding);
 
-    val accessible =
-      (case private of
-        NONE => true
-      | SOME scope => member (op =) scopes scope);
+    val limitation =
+      (case limited of
+        NONE => NONE
+      | SOME (strict, scope) => if member (op =) scopes scope then NONE else SOME strict);
 
     val spec1 =
       maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path @ prefix @ qualifier);
@@ -192,7 +196,7 @@
     val _ =
       exists (fn (a, _) => member (op =) bad_specs a orelse exists_string (fn s => s = "\"") a) spec
       andalso error (bad binding);
-  in {accessible = accessible, concealed = concealed, spec = if null spec2 then [] else spec} end;
+  in {limitation = limitation, concealed = concealed, spec = if null spec2 then [] else spec} end;
 
 end;
 
diff -r f84b93187ab6 -r 7d46aa03696e src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Mon Apr 06 17:28:07 2015 +0200
+++ b/src/Pure/General/name_space.ML	Mon Apr 06 22:11:01 2015 +0200
@@ -35,8 +35,11 @@
   val get_scopes: naming -> Binding.scope list
   val get_scope: naming -> Binding.scope option
   val new_scope: naming -> Binding.scope * naming
+  val limited: bool -> Position.T -> naming -> naming
   val private_scope: Binding.scope -> naming -> naming
   val private: Position.T -> naming -> naming
+  val restricted_scope: Binding.scope -> naming -> naming
+  val restricted: Position.T -> naming -> naming
   val concealed: naming -> naming
   val get_group: naming -> serial option
   val set_group: serial option -> naming -> naming
@@ -297,62 +300,73 @@
 
 datatype naming = Naming of
  {scopes: Binding.scope list,
-  private: Binding.scope option,
+  limited: (bool * Binding.scope) option,
   concealed: bool,
   group: serial option,
   theory_name: string,
   path: (string * bool) list};
 
-fun make_naming (scopes, private, concealed, group, theory_name, path) =
-  Naming {scopes = scopes, private = private, concealed = concealed,
+fun make_naming (scopes, limited, concealed, group, theory_name, path) =
+  Naming {scopes = scopes, limited = limited, concealed = concealed,
     group = group, theory_name = theory_name, path = path};
 
-fun map_naming f (Naming {scopes, private, concealed, group, theory_name, path}) =
-  make_naming (f (scopes, private, concealed, group, theory_name, path));
+fun map_naming f (Naming {scopes, limited, concealed, group, theory_name, path}) =
+  make_naming (f (scopes, limited, concealed, group, theory_name, path));
 
-fun map_path f = map_naming (fn (scopes, private, concealed, group, theory_name, path) =>
-  (scopes, private, concealed, group, theory_name, f path));
 
+(* scope and access limitation *)
 
 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 ();
     val naming' =
-      naming |> map_naming (fn (scopes, private, concealed, group, theory_name, path) =>
-        (scope :: scopes, private, concealed, group, theory_name, path));
+      naming |> map_naming (fn (scopes, limited, concealed, group, theory_name, path) =>
+        (scope :: scopes, limited, concealed, group, theory_name, path));
   in (scope, naming') end;
 
-fun private_scope scope = map_naming (fn (scopes, _, concealed, group, theory_name, path) =>
-  (scopes, SOME scope, concealed, group, theory_name, path));
+fun limited_scope strict scope =
+  map_naming (fn (scopes, _, concealed, group, theory_name, path) =>
+    (scopes, SOME (strict, scope), concealed, group, theory_name, path));
 
-fun private pos naming =
+fun limited strict pos naming =
   (case get_scope naming of
-    SOME scope => private_scope scope naming
-  | NONE => error ("Missing local scope -- cannot declare private names" ^ Position.here pos));
+    SOME scope => limited_scope strict scope naming
+  | NONE => error ("Missing local scope -- cannot limit name space accesses" ^ Position.here pos));
+
+val private_scope = limited_scope true;
+val private = limited true;
+
+val restricted_scope = limited_scope false;
+val restricted = limited false;
 
-val concealed = map_naming (fn (scopes, private, _, group, theory_name, path) =>
-  (scopes, private, true, group, theory_name, path));
+val concealed = map_naming (fn (scopes, limited, _, group, theory_name, path) =>
+  (scopes, limited, true, group, theory_name, path));
+
 
-fun set_theory_name theory_name = map_naming (fn (scopes, private, concealed, group, _, path) =>
-  (scopes, private, concealed, group, theory_name, path));
+(* additional structural info *)
+
+fun set_theory_name theory_name = map_naming (fn (scopes, limited, concealed, group, _, path) =>
+  (scopes, limited, concealed, group, theory_name, path));
 
 fun get_group (Naming {group, ...}) = group;
 
-fun set_group group = map_naming (fn (scopes, private, concealed, _, theory_name, path) =>
-  (scopes, private, concealed, group, theory_name, path));
+fun set_group group = map_naming (fn (scopes, limited, concealed, _, theory_name, path) =>
+  (scopes, limited, concealed, group, theory_name, path));
 
 fun new_group naming = set_group (SOME (serial ())) naming;
 val reset_group = set_group NONE;
 
+
+(* name entry path *)
+
 fun get_path (Naming {path, ...}) = path;
 
+fun map_path f = map_naming (fn (scopes, limited, concealed, group, theory_name, path) =>
+  (scopes, limited, concealed, group, theory_name, f path));
+
 fun add_path elems = map_path (fn path => path @ [(elems, false)]);
 val root_path = map_path (fn _ => []);
 val parent_path = map_path (perhaps (try (#1 o split_last)));
@@ -365,14 +379,16 @@
 val local_naming = global_naming |> add_path Long_Name.localN;
 
 
-(* visibility flags *)
+(* transform *)
 
-fun transform_naming (Naming {private = private', concealed = concealed', ...}) =
-  fold private_scope (the_list private') #>
+fun transform_naming (Naming {limited = limited', concealed = concealed', ...}) =
+  (case limited' of
+    SOME (strict, scope) => limited_scope strict scope
+  | NONE => I) #>
   concealed' ? concealed;
 
-fun transform_binding (Naming {private, concealed, ...}) =
-  Binding.private_default private #>
+fun transform_binding (Naming {limited, concealed, ...}) =
+  Binding.limited_default limited #>
   concealed ? Binding.concealed;
 
 
@@ -400,11 +416,12 @@
 
 fun accesses naming binding =
   (case name_spec naming binding of
-    {accessible = false, ...} => ([], [])
-  | {spec, ...} =>
+    {limitation = SOME true, ...} => ([], [])
+  | {limitation, spec, ...} =>
       let
-        val sfxs = mandatory_suffixes spec;
-        val pfxs = mandatory_prefixes spec;
+        val restrict = is_some limitation ? filter (fn [_] => false | _ => true);
+        val sfxs = restrict (mandatory_suffixes spec);
+        val pfxs = restrict (mandatory_prefixes spec);
       in apply2 (map Long_Name.implode) (sfxs @ pfxs, sfxs) end);
 
 
diff -r f84b93187ab6 -r 7d46aa03696e src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Mon Apr 06 17:28:07 2015 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Mon Apr 06 22:11:01 2015 +0200
@@ -44,7 +44,8 @@
 
 datatype command_parser =
   Parser of (Toplevel.transition -> Toplevel.transition) parser |
-  Private_Parser of Position.T option -> (Toplevel.transition -> Toplevel.transition) parser;
+  Limited_Parser of
+    (bool * Position.T) option -> (Toplevel.transition -> Toplevel.transition) parser;
 
 datatype command = Command of
  {comment: string,
@@ -145,8 +146,8 @@
 
 fun local_theory_command trans command_keyword comment parse =
   raw_command command_keyword comment
-    (Private_Parser (fn private =>
-      Parse.opt_target -- parse >> (fn (target, f) => trans private target f)));
+    (Limited_Parser (fn limited =>
+      Parse.opt_target -- parse >> (fn (target, f) => trans limited target f)));
 
 val local_theory' = local_theory_command Toplevel.local_theory';
 val local_theory = local_theory_command Toplevel.local_theory;
@@ -161,8 +162,11 @@
 
 local
 
+val before_command =
+  Scan.option (Parse.position (Parse.private >> K true || Parse.restricted >> K false));
+
 fun parse_command thy =
-  Scan.ahead (Parse.opt_private |-- Parse.position Parse.command_) :|-- (fn (name, pos) =>
+  Scan.ahead (before_command |-- Parse.position Parse.command_) :|-- (fn (name, pos) =>
     let
       val command_tags = Parse.command_ -- Parse.tags;
       val tr0 = Toplevel.empty |> Toplevel.name name |> Toplevel.position pos;
@@ -170,9 +174,9 @@
       (case lookup_commands thy name of
         SOME (Command {command_parser = Parser parse, ...}) =>
           Parse.!!! (command_tags |-- parse) >> (fn f => f tr0)
-      | SOME (Command {command_parser = Private_Parser parse, ...}) =>
-          Parse.opt_private :|-- (fn private =>
-            Parse.!!! (command_tags |-- parse private)) >> (fn f => f tr0)
+      | SOME (Command {command_parser = Limited_Parser parse, ...}) =>
+          before_command :|-- (fn limited =>
+            Parse.!!! (command_tags |-- parse limited)) >> (fn f => f tr0)
       | NONE =>
           Scan.succeed
             (tr0 |> Toplevel.imperative (fn () => err_command "Undefined command " name [pos])))
@@ -225,9 +229,9 @@
 
 fun parse tok (result, content, improper) =
   if Token.is_improper tok then (result, content, tok :: improper)
-  else if Token.is_private tok orelse
+  else if Token.is_command_modifier tok orelse
     Token.is_command tok andalso
-      (not (exists Token.is_private content) orelse exists Token.is_command content)
+      (not (exists Token.is_command_modifier content) orelse exists Token.is_command content)
   then (flush (result, content, improper), [tok], [])
   else (result, tok :: (improper @ content), []);
 
diff -r f84b93187ab6 -r 7d46aa03696e src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Mon Apr 06 17:28:07 2015 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Mon Apr 06 22:11:01 2015 +0200
@@ -219,8 +219,8 @@
 
     for (tok <- toks) {
       if (tok.is_improper) improper += tok
-      else if (tok.is_private ||
-        tok.is_command && (!content.exists(_.is_private) || content.exists(_.is_command)))
+      else if (tok.is_command_modifier ||
+        tok.is_command && (!content.exists(_.is_command_modifier) || content.exists(_.is_command)))
       { flush(); content += tok }
       else { content ++= improper; improper.clear; content += tok }
     }
diff -r f84b93187ab6 -r 7d46aa03696e src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Mon Apr 06 17:28:07 2015 +0200
+++ b/src/Pure/Isar/parse.ML	Mon Apr 06 22:11:01 2015 +0200
@@ -104,7 +104,7 @@
   val propp: (string * string list) parser
   val termp: (string * string list) parser
   val private: Position.T parser
-  val opt_private: Position.T option parser
+  val restricted: Position.T parser
   val target: (xstring * Position.T) parser
   val opt_target: (xstring * Position.T) option parser
   val args: Token.T list parser
@@ -401,7 +401,7 @@
 (* target information *)
 
 val private = position ($$$ "private") >> #2;
-val opt_private = Scan.option private;
+val restricted = position ($$$ "restricted") >> #2;
 
 val target = ($$$ "(" -- $$$ "in") |-- !!! (position xname --| $$$ ")");
 val opt_target = Scan.option target;
diff -r f84b93187ab6 -r 7d46aa03696e src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Apr 06 17:28:07 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Apr 06 22:11:01 2015 +0200
@@ -38,6 +38,8 @@
   val new_scope: Proof.context -> Binding.scope * Proof.context
   val private_scope: Binding.scope -> Proof.context -> Proof.context
   val private: Position.T -> Proof.context -> Proof.context
+  val restricted_scope: Binding.scope -> Proof.context -> Proof.context
+  val restricted: 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
@@ -319,6 +321,9 @@
 
 val private_scope = map_naming o Name_Space.private_scope;
 val private = map_naming o Name_Space.private;
+val restricted_scope = map_naming o Name_Space.restricted_scope;
+val restricted = map_naming o Name_Space.restricted;
+
 val concealed = map_naming Name_Space.concealed;
 
 
diff -r f84b93187ab6 -r 7d46aa03696e src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Mon Apr 06 17:28:07 2015 +0200
+++ b/src/Pure/Isar/token.ML	Mon Apr 06 22:11:01 2015 +0200
@@ -46,7 +46,7 @@
   val is_command: T -> bool
   val is_name: T -> bool
   val keyword_with: (string -> bool) -> T -> bool
-  val is_private: T -> bool
+  val is_command_modifier: T -> bool
   val ident_with: (string -> bool) -> T -> bool
   val is_proper: T -> bool
   val is_improper: T -> bool
@@ -247,7 +247,7 @@
 fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x
   | keyword_with _ _ = false;
 
-val is_private = keyword_with (fn x => x = "private");
+val is_command_modifier = keyword_with (fn x => x = "private" orelse x = "restricted");
 
 fun ident_with pred (Token (_, (Ident, x), _)) = pred x
   | ident_with _ _ = false;
diff -r f84b93187ab6 -r 7d46aa03696e src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Mon Apr 06 17:28:07 2015 +0200
+++ b/src/Pure/Isar/token.scala	Mon Apr 06 22:11:01 2015 +0200
@@ -259,7 +259,8 @@
   def is_begin: Boolean = is_keyword && source == "begin"
   def is_end: Boolean = is_command && source == "end"
 
-  def is_private: Boolean = is_keyword && source == "private"
+  def is_command_modifier: Boolean =
+    is_keyword && (source == "private" || source == "restricted")
 
   def is_begin_block: Boolean = is_command && source == "{"
   def is_end_block: Boolean = is_command && source == "}"
diff -r f84b93187ab6 -r 7d46aa03696e src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon Apr 06 17:28:07 2015 +0200
+++ b/src/Pure/Isar/toplevel.ML	Mon Apr 06 22:11:01 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': Position.T option -> (xstring * Position.T) option ->
+  val local_theory': (bool * Position.T) option -> (xstring * Position.T) option ->
     (bool -> local_theory -> local_theory) -> transition -> transition
-  val local_theory: Position.T option -> (xstring * Position.T) option ->
+  val local_theory: (bool * 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': Position.T option -> (xstring * Position.T) option ->
+  val local_theory_to_proof': (bool * Position.T) option -> (xstring * Position.T) option ->
     (bool -> local_theory -> Proof.state) -> transition -> transition
-  val local_theory_to_proof: Position.T option -> (xstring * Position.T) option ->
+  val local_theory_to_proof: (bool * 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,12 +412,15 @@
         | NONE => raise UNDEF)
     | _ => raise UNDEF));
 
-fun local_theory' private target f = present_transaction (fn int =>
+val limited_context =
+  fn SOME (strict, scope) => Proof_Context.map_naming (Name_Space.limited strict scope) | NONE => I;
+
+fun local_theory' limited target f = present_transaction (fn int =>
   (fn Theory (gthy, _) =>
         let
           val (finish, lthy) = Named_Target.switch target gthy;
           val lthy' = lthy
-            |> fold Proof_Context.private (the_list private)
+            |> limited_context limited
             |> Local_Theory.new_group
             |> f int
             |> Local_Theory.reset_group;
@@ -425,7 +428,7 @@
     | _ => raise UNDEF))
   (K ());
 
-fun local_theory private target f = local_theory' private target (K f);
+fun local_theory limited target f = local_theory' limited target (K f);
 
 fun present_local_theory target = present_transaction (fn int =>
   (fn Theory (gthy, _) =>
@@ -470,18 +473,18 @@
 
 in
 
-fun local_theory_to_proof' private target f = begin_proof
+fun local_theory_to_proof' limited target f = begin_proof
   (fn int => fn gthy =>
     let
       val (finish, lthy) = Named_Target.switch target gthy;
       val prf = lthy
-        |> fold Proof_Context.private (the_list private)
+        |> limited_context limited
         |> Local_Theory.new_group
         |> f int;
     in (finish o Local_Theory.reset_group, prf) end);
 
-fun local_theory_to_proof private target f =
-  local_theory_to_proof' private target (K f);
+fun local_theory_to_proof limited target f =
+  local_theory_to_proof' limited target (K f);
 
 fun theory_to_proof f = begin_proof
   (fn _ => fn gthy =>
diff -r f84b93187ab6 -r 7d46aa03696e src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Mon Apr 06 17:28:07 2015 +0200
+++ b/src/Pure/Pure.thy	Mon Apr 06 22:11:01 2015 +0200
@@ -11,8 +11,8 @@
     "\<subseteq>" "]" "assumes" "attach" "binder" "constrains"
     "defines" "fixes" "for" "identifier" "if" "in" "includes" "infix"
     "infixl" "infixr" "is" "notes" "obtains" "open" "output"
-    "overloaded" "pervasive" "private" "shows" "structure" "unchecked"
-    "where" "|"
+    "overloaded" "pervasive" "private" "restricted" "shows"
+    "structure" "unchecked" "where" "|"
   and "text" "txt" :: document_body
   and "text_raw" :: document_raw
   and "default_sort" :: thy_decl == ""
diff -r f84b93187ab6 -r 7d46aa03696e src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Mon Apr 06 17:28:07 2015 +0200
+++ b/src/Pure/Thy/thy_output.ML	Mon Apr 06 22:11:01 2015 +0200
@@ -384,10 +384,10 @@
         in (SOME (name, pos', tags), (mk (name, source), (flag, d))) end));
 
     val command = Scan.peek (fn d =>
-      Scan.optional (Scan.one Token.is_private -- improper >> op ::) [] --
+      Scan.optional (Scan.one Token.is_command_modifier -- improper >> op ::) [] --
       Scan.one Token.is_command -- Scan.repeat tag
-      >> (fn ((private, cmd), tags) =>
-        map (fn tok => (NONE, (Basic_Token tok, ("", d)))) private @
+      >> (fn ((cmd_mod, cmd), tags) =>
+        map (fn tok => (NONE, (Basic_Token tok, ("", d)))) cmd_mod @
           [(SOME (Token.content_of cmd, Token.pos_of cmd, tags),
             (Basic_Token cmd, (Latex.markup_false, d)))]));
 
diff -r f84b93187ab6 -r 7d46aa03696e src/Pure/sign.ML
--- a/src/Pure/sign.ML	Mon Apr 06 17:28:07 2015 +0200
+++ b/src/Pure/sign.ML	Mon Apr 06 22:11:01 2015 +0200
@@ -525,6 +525,8 @@
 
 val private_scope = map_naming o Name_Space.private_scope;
 val private = map_naming o Name_Space.private;
+val restricted_scope = map_naming o Name_Space.restricted_scope;
+val restricted = map_naming o Name_Space.restricted;
 val concealed = map_naming Name_Space.concealed;
 
 
diff -r f84b93187ab6 -r 7d46aa03696e src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Mon Apr 06 17:28:07 2015 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Mon Apr 06 22:11:01 2015 +0200
@@ -274,11 +274,11 @@
   {
     def maybe_command_start(i: Text.Offset): Option[Text.Info[Token]] =
       token_reverse_iterator(syntax, buffer, i).
-        find(info => info.info.is_private || info.info.is_command)
+        find(info => info.info.is_command_modifier || info.info.is_command)
 
     def maybe_command_stop(i: Text.Offset): Option[Text.Info[Token]] =
       token_iterator(syntax, buffer, i).
-        find(info => info.info.is_private || info.info.is_command)
+        find(info => info.info.is_command_modifier || info.info.is_command)
 
     if (JEdit_Lib.buffer_range(buffer).contains(offset)) {
       val start_info =
@@ -288,15 +288,15 @@
           case Some(Text.Info(range1, tok1)) if tok1.is_command =>
             val info2 = maybe_command_start(range1.start - 1)
             info2 match {
-              case Some(Text.Info(_, tok2)) if tok2.is_private => info2
+              case Some(Text.Info(_, tok2)) if tok2.is_command_modifier => info2
               case _ => info1
             }
           case _ => info1
         }
       }
-      val (start_is_private, start, start_next) =
+      val (start_is_command_modifier, start, start_next) =
         start_info match {
-          case Some(Text.Info(range, tok)) => (tok.is_private, range.start, range.stop)
+          case Some(Text.Info(range, tok)) => (tok.is_command_modifier, range.start, range.stop)
           case None => (false, 0, 0)
         }
 
@@ -304,7 +304,7 @@
       {
         val info1 = maybe_command_stop(start_next)
         info1 match {
-          case Some(Text.Info(range1, tok1)) if tok1.is_command && start_is_private =>
+          case Some(Text.Info(range1, tok1)) if tok1.is_command && start_is_command_modifier =>
             maybe_command_stop(range1.stop)
           case _ => info1
         }