# HG changeset patch
# User wenzelm
# Date 1427833865 -7200
# Node ID e0dc738eb08c3421241bbfdf2611cba6c9eb0898
# Parent  3470a265d404d85f3441c8bab976a0295fe54f7b
support for explicit scope of private entries;

diff -r 3470a265d404 -r e0dc738eb08c src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Tue Mar 31 21:12:22 2015 +0200
+++ b/src/Pure/General/binding.ML	Tue Mar 31 22:31:05 2015 +0200
@@ -9,6 +9,8 @@
 
 signature BINDING =
 sig
+  eqtype scope
+  val new_scope: unit -> scope
   eqtype binding
   val path_of: binding -> (string * bool) list
   val make: bstring * Position.T -> binding
@@ -28,15 +30,16 @@
   val prefix_of: binding -> (string * bool) list
   val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding
   val prefix: bool -> string -> binding -> binding
-  val private: binding -> binding
+  val private: scope -> binding -> binding
+  val private_default: scope option -> binding -> binding
   val concealed: binding -> binding
   val pretty: binding -> Pretty.T
   val print: binding -> string
   val pp: binding -> Pretty.T
   val bad: binding -> string
   val check: binding -> unit
-  val name_spec: (string * bool) list -> binding ->
-    {private: bool, concealed: bool, spec: (string * bool) list}
+  val name_spec: scope list -> (string * bool) list -> binding ->
+    {accessible: bool, concealed: bool, spec: (string * bool) list}
 end;
 
 structure Binding: BINDING =
@@ -44,10 +47,17 @@
 
 (** representation **)
 
-(* datatype *)
+(* scope of private entries *)
+
+datatype scope = Scope of serial;
+
+fun new_scope () = Scope (serial ());
+
+
+(* binding *)
 
 datatype binding = Binding of
- {private: bool,                    (*entry is strictly private -- no name space accesses*)
+ {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*)
@@ -69,7 +79,7 @@
 
 (* name and position *)
 
-fun make (name, pos) = make_binding (false, false, [], [], name, pos);
+fun make (name, pos) = make_binding (NONE, false, [], [], name, pos);
 
 fun pos_of (Binding {pos, ...}) = pos;
 fun set_pos pos =
@@ -107,7 +117,7 @@
 fun qualified_name "" = empty
   | qualified_name s =
       let val (qualifier, name) = split_last (Long_Name.explode s)
-      in make_binding (false, false, [], map (rpair false) qualifier, name, Position.none) end;
+      in make_binding (NONE, false, [], map (rpair false) qualifier, name, Position.none) end;
 
 
 (* system prefix *)
@@ -124,9 +134,13 @@
 
 (* visibility flags *)
 
-val private =
+fun private scope =
   map_binding (fn (_, concealed, prefix, qualifier, name, pos) =>
-    (true, concealed, prefix, qualifier, name, pos));
+    (SOME 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 concealed =
   map_binding (fn (private, _, prefix, qualifier, name, pos) =>
@@ -161,11 +175,16 @@
 
 val bad_specs = ["", "??", "__"];
 
-fun name_spec path binding =
+fun name_spec scopes path binding =
   let
     val Binding {private, 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 spec1 =
       maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path @ prefix @ qualifier);
     val spec2 = if name = "" then [] else [(name, true)];
@@ -173,7 +192,7 @@
     val _ =
       exists (fn (a, _) => member (op =) bad_specs a orelse exists_string (fn s => s = "\"") a) spec
       andalso error (bad binding);
-  in {private = private, concealed = concealed, spec = if null spec2 then [] else spec} end;
+  in {accessible = accessible, concealed = concealed, spec = if null spec2 then [] else spec} end;
 
 end;
 
diff -r 3470a265d404 -r e0dc738eb08c src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Tue Mar 31 21:12:22 2015 +0200
+++ b/src/Pure/General/name_space.ML	Tue Mar 31 22:31:05 2015 +0200
@@ -32,7 +32,9 @@
   val completion: Context.generic -> T -> xstring * Position.T -> Completion.T
   val merge: T * T -> T
   type naming
-  val private: naming -> naming
+  val get_scope: naming -> Binding.scope option
+  val new_scope: naming -> Binding.scope * naming
+  val private: Binding.scope -> naming -> naming
   val concealed: naming -> naming
   val get_group: naming -> serial option
   val set_group: serial option -> naming -> naming
@@ -280,37 +282,48 @@
 (* datatype naming *)
 
 datatype naming = Naming of
- {private: bool,
+ {scopes: Binding.scope list,
+  private: Binding.scope option,
   concealed: bool,
   group: serial option,
   theory_name: string,
   path: (string * bool) list};
 
-fun make_naming (private, concealed, group, theory_name, path) =
-  Naming {private = private, concealed = concealed, group = group,
-    theory_name = theory_name, path = path};
+fun make_naming (scopes, private, concealed, group, theory_name, path) =
+  Naming {scopes = scopes, private = private, concealed = concealed,
+    group = group, theory_name = theory_name, path = path};
 
-fun map_naming f (Naming {private, concealed, group, theory_name, path}) =
-  make_naming (f (private, concealed, group, theory_name, 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_path f = map_naming (fn (private, concealed, group, theory_name, path) =>
-  (private, concealed, group, theory_name, f path));
+fun map_path f = map_naming (fn (scopes, private, concealed, group, theory_name, path) =>
+  (scopes, private, concealed, group, theory_name, f path));
 
 
-val private = map_naming (fn (_, concealed, group, theory_name, path) =>
-  (true, concealed, group, theory_name, path));
+fun get_scopes (Naming {scopes, ...}) = scopes;
+val get_scope = try hd o get_scopes;
 
-val concealed = map_naming (fn (private, _, group, theory_name, path) =>
-  (private, true, 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));
+  in (scope, naming') end;
 
-fun set_theory_name theory_name = map_naming (fn (private, concealed, group, _, path) =>
-  (private, concealed, group, theory_name, path));
+fun private scope = map_naming (fn (scopes, _, concealed, group, theory_name, path) =>
+  (scopes, SOME scope, concealed, group, theory_name, path));
 
+val concealed = map_naming (fn (scopes, private, _, group, theory_name, path) =>
+  (scopes, private, 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));
 
 fun get_group (Naming {group, ...}) = group;
 
-fun set_group group = map_naming (fn (private, concealed, _, theory_name, path) =>
-  (private, concealed, group, theory_name, path));
+fun set_group group = map_naming (fn (scopes, private, concealed, _, theory_name, path) =>
+  (scopes, private, concealed, group, theory_name, path));
 
 fun new_group naming = set_group (SOME (serial ())) naming;
 val reset_group = set_group NONE;
@@ -325,18 +338,18 @@
 fun qualified_path mandatory binding = map_path (fn path =>
   path @ Binding.path_of (Binding.qualified mandatory "" binding));
 
-val global_naming = make_naming (false, false, NONE, "", []);
+val global_naming = make_naming ([], NONE, false, NONE, "", []);
 val local_naming = global_naming |> add_path Long_Name.localN;
 
 
 (* full name *)
 
 fun transform_binding (Naming {private, concealed, ...}) =
-  private ? Binding.private #>
+  Binding.private_default private #>
   concealed ? Binding.concealed;
 
 fun name_spec naming binding =
-  Binding.name_spec (get_path naming) (transform_binding naming binding);
+  Binding.name_spec (get_scopes naming) (get_path naming) (transform_binding naming binding);
 
 fun full_name naming =
   name_spec naming #> #spec #> map #1 #> Long_Name.implode;
@@ -357,7 +370,7 @@
 
 fun accesses naming binding =
   (case name_spec naming binding of
-    {private = true, ...} => ([], [])
+    {accessible = false, ...} => ([], [])
   | {spec, ...} =>
       let
         val sfxs = mandatory_suffixes spec;
diff -r 3470a265d404 -r e0dc738eb08c src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Tue Mar 31 21:12:22 2015 +0200
+++ b/src/Pure/Isar/local_theory.ML	Tue Mar 31 22:31:05 2015 +0200
@@ -144,9 +144,13 @@
     else lthy
   end;
 
-fun open_target background_naming operations after_close target =
-  assert target
-  |> Data.map (cons (make_lthy (background_naming, operations, after_close, true, target)));
+fun open_target background_naming operations after_close lthy =
+  let
+    val _ = assert lthy;
+    val (_, target) = Proof_Context.new_scope lthy;
+  in
+    target |> Data.map (cons (make_lthy (background_naming, operations, after_close, true, target)))
+  end;
 
 fun close_target lthy =
   let
diff -r 3470a265d404 -r e0dc738eb08c src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Mar 31 21:12:22 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Mar 31 22:31:05 2015 +0200
@@ -34,6 +34,8 @@
   val naming_of: Proof.context -> Name_Space.naming
   val restore_naming: Proof.context -> Proof.context -> Proof.context
   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 concealed: Proof.context -> Proof.context
   val class_space: Proof.context -> Name_Space.T
   val type_space: Proof.context -> Name_Space.T
@@ -305,6 +307,14 @@
 
 val full_name = Name_Space.full_name o naming_of;
 
+val get_scope = Name_Space.get_scope o naming_of;
+
+fun new_scope ctxt =
+  let
+    val (scope, naming') = Name_Space.new_scope (naming_of ctxt);
+    val ctxt' = map_naming (K naming') ctxt;
+  in (scope, ctxt') end;
+
 val concealed = map_naming Name_Space.concealed;
 
 
diff -r 3470a265d404 -r e0dc738eb08c src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue Mar 31 21:12:22 2015 +0200
+++ b/src/Pure/sign.ML	Tue Mar 31 22:31:05 2015 +0200
@@ -101,6 +101,8 @@
     (string * (Proof.context -> Ast.ast list -> Ast.ast)) list -> theory -> theory
   val add_trrules: Ast.ast Syntax.trrule list -> theory -> theory
   val del_trrules: Ast.ast Syntax.trrule list -> theory -> theory
+  val get_scope: theory -> Binding.scope option
+  val new_scope: theory -> Binding.scope * theory
   val new_group: theory -> theory
   val reset_group: theory -> theory
   val add_path: string -> theory -> theory
@@ -500,6 +502,14 @@
 
 (* naming *)
 
+val get_scope = Name_Space.get_scope o naming_of;
+
+fun new_scope thy =
+  let
+    val (scope, naming') = Name_Space.new_scope (naming_of thy);
+    val thy' = map_naming (K naming') thy;
+  in (scope, thy') end;
+
 val new_group = map_naming Name_Space.new_group;
 val reset_group = map_naming Name_Space.reset_group;