src/Pure/General/binding.ML

--- a/src/Pure/General/binding.ML	Mon Mar 30 20:51:11 2015 +0200
+++ b/src/Pure/General/binding.ML	Mon Mar 30 22:34:59 2015 +0200
@@ -10,7 +10,8 @@
 signature BINDING =
 sig
   eqtype binding
-  val dest: binding -> bool * (string * bool) list * bstring
+  val dest: binding -> {private: bool, conceal: bool, path: (string * bool) list, name: bstring}
+  val path_of: binding -> (string * bool) list
   val make: bstring * Position.T -> binding
   val pos_of: binding -> Position.T
   val set_pos: Position.T -> binding -> binding
@@ -28,6 +29,7 @@
   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 conceal: binding -> binding
   val pretty: binding -> Pretty.T
   val print: binding -> string
@@ -44,20 +46,24 @@
 (* datatype *)
 
 datatype binding = Binding of
- {conceal: bool,                    (*internal -- for foundational purposes only*)
+ {private: bool,                    (*entry is strictly private -- no name space accesses*)
+  conceal: 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 (conceal, prefix, qualifier, name, pos) =
-  Binding {conceal = conceal, prefix = prefix, qualifier = qualifier, name = name, pos = pos};
+fun make_binding (private, conceal, prefix, qualifier, name, pos) =
+  Binding {private = private, conceal = conceal, prefix = prefix,
+    qualifier = qualifier, name = name, pos = pos};
 
-fun map_binding f (Binding {conceal, prefix, qualifier, name, pos}) =
-  make_binding (f (conceal, prefix, qualifier, name, pos));
+fun map_binding f (Binding {private, conceal, prefix, qualifier, name, pos}) =
+  make_binding (f (private, conceal, prefix, qualifier, name, pos));
 
-fun dest (Binding {conceal, prefix, qualifier, name, ...}) =
-  (conceal, prefix @ qualifier, name);
+fun dest (Binding {private, conceal, prefix, qualifier, name, ...}) =
+  {private = private, conceal = conceal, path = prefix @ qualifier, name = name};
+
+val path_of = #path o dest;
 
 
 
@@ -65,11 +71,12 @@
 
 (* name and position *)
 
-fun make (name, pos) = make_binding (false, [], [], name, pos);
+fun make (name, pos) = make_binding (false, false, [], [], name, pos);
 
 fun pos_of (Binding {pos, ...}) = pos;
 fun set_pos pos =
-  map_binding (fn (conceal, prefix, qualifier, name, _) => (conceal, prefix, qualifier, name, pos));
+  map_binding (fn (private, conceal, prefix, qualifier, name, _) =>
+    (private, conceal, prefix, qualifier, name, pos));
 
 fun name name = make (name, Position.none);
 fun name_of (Binding {name, ...}) = name;
@@ -77,8 +84,8 @@
 fun eq_name (b, b') = name_of b = name_of b';
 
 fun map_name f =
-  map_binding (fn (conceal, prefix, qualifier, name, pos) =>
-    (conceal, prefix, qualifier, f name, pos));
+  map_binding (fn (private, conceal, prefix, qualifier, name, pos) =>
+    (private, conceal, prefix, qualifier, f name, pos));
 
 val prefix_name = map_name o prefix;
 val suffix_name = map_name o suffix;
@@ -91,17 +98,18 @@
 
 fun qualify _ "" = I
   | qualify mandatory qual =
-      map_binding (fn (conceal, prefix, qualifier, name, pos) =>
-        (conceal, prefix, (qual, mandatory) :: qualifier, name, pos));
+      map_binding (fn (private, conceal, prefix, qualifier, name, pos) =>
+        (private, conceal, prefix, (qual, mandatory) :: qualifier, name, pos));
 
-fun qualified mandatory name' = map_binding (fn (conceal, prefix, qualifier, name, pos) =>
-  let val qualifier' = if name = "" then qualifier else qualifier @ [(name, mandatory)]
-  in (conceal, prefix, qualifier', name', pos) end);
+fun qualified mandatory name' =
+  map_binding (fn (private, conceal, prefix, qualifier, name, pos) =>
+    let val qualifier' = if name = "" then qualifier else qualifier @ [(name, mandatory)]
+    in (private, conceal, prefix, qualifier', name', pos) end);
 
 fun qualified_name "" = empty
   | qualified_name s =
       let val (qualifier, name) = split_last (Long_Name.explode s)
-      in make_binding (false, [], map (rpair false) qualifier, name, Position.none) end;
+      in make_binding (false, false, [], map (rpair false) qualifier, name, Position.none) end;
 
 
 (* system prefix *)
@@ -109,18 +117,22 @@
 fun prefix_of (Binding {prefix, ...}) = prefix;
 
 fun map_prefix f =
-  map_binding (fn (conceal, prefix, qualifier, name, pos) =>
-    (conceal, f prefix, qualifier, name, pos));
+  map_binding (fn (private, conceal, prefix, qualifier, name, pos) =>
+    (private, conceal, f prefix, qualifier, name, pos));
 
 fun prefix _ "" = I
   | prefix mandatory prfx = map_prefix (cons (prfx, mandatory));
 
 
-(* conceal *)
+(* visibility flags *)
+
+val private =
+  map_binding (fn (_, conceal, prefix, qualifier, name, pos) =>
+    (true, conceal, prefix, qualifier, name, pos));
 
 val conceal =
-  map_binding (fn (_, prefix, qualifier, name, pos) =>
-    (true, prefix, qualifier, name, pos));
+  map_binding (fn (private, _, prefix, qualifier, name, pos) =>
+    (private, true, prefix, qualifier, name, pos));
 
 
 (* print *)
@@ -148,4 +160,3 @@
 end;
 
 type binding = Binding.binding;
-