src/Pure/General/binding.ML

--- a/src/Pure/General/binding.ML	Sun Oct 25 11:58:11 2009 +0100
+++ b/src/Pure/General/binding.ML	Sun Oct 25 12:27:21 2009 +0100
@@ -10,7 +10,7 @@
 signature BINDING =
 sig
   type binding
-  val dest: binding -> (string * bool) list * bstring
+  val dest: binding -> bool * (string * bool) list * bstring
   val make: bstring * Position.T -> binding
   val pos_of: binding -> Position.T
   val name: bstring -> binding
@@ -27,6 +27,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 conceal: binding -> binding
   val str_of: binding -> string
 end;
 
@@ -38,19 +39,21 @@
 (* datatype *)
 
 abstype binding = Binding of
- {prefix: (string * bool) list,     (*system prefix*)
+ {conceal: bool,                    (*internal -- for foundational purposes only*)
+  prefix: (string * bool) list,     (*system prefix*)
   qualifier: (string * bool) list,  (*user qualifier*)
   name: bstring,                    (*base name*)
   pos: Position.T}                  (*source position*)
 with
 
-fun make_binding (prefix, qualifier, name, pos) =
-  Binding {prefix = prefix, qualifier = qualifier, name = name, pos = pos};
+fun make_binding (conceal, prefix, qualifier, name, pos) =
+  Binding {conceal = conceal, prefix = prefix, qualifier = qualifier, name = name, pos = pos};
 
-fun map_binding f (Binding {prefix, qualifier, name, pos}) =
-  make_binding (f (prefix, qualifier, name, pos));
+fun map_binding f (Binding {conceal, prefix, qualifier, name, pos}) =
+  make_binding (f (conceal, prefix, qualifier, name, pos));
 
-fun dest (Binding {prefix, qualifier, name, ...}) = (prefix @ qualifier, name);
+fun dest (Binding {conceal, prefix, qualifier, name, ...}) =
+  (conceal, prefix @ qualifier, name);
 
 
 
@@ -58,7 +61,7 @@
 
 (* name and position *)
 
-fun make (name, pos) = make_binding ([], [], name, pos);
+fun make (name, pos) = make_binding (false, [], [], name, pos);
 fun name name = make (name, Position.none);
 
 fun pos_of (Binding {pos, ...}) = pos;
@@ -66,7 +69,10 @@
 
 fun eq_name (b, b') = name_of b = name_of b';
 
-fun map_name f = map_binding (fn (prefix, qualifier, name, pos) => (prefix, qualifier, f name, pos));
+fun map_name f =
+  map_binding (fn (conceal, prefix, qualifier, name, pos) =>
+    (conceal, prefix, qualifier, f name, pos));
+
 val prefix_name = map_name o prefix;
 val suffix_name = map_name o suffix;
 
@@ -77,13 +83,14 @@
 (* user qualifier *)
 
 fun qualify _ "" = I
-  | qualify mandatory qual = map_binding (fn (prefix, qualifier, name, pos) =>
-      (prefix, (qual, mandatory) :: qualifier, name, pos));
+  | qualify mandatory qual =
+      map_binding (fn (conceal, prefix, qualifier, name, pos) =>
+        (conceal, prefix, (qual, mandatory) :: qualifier, name, pos));
 
 fun qualified_name "" = empty
   | qualified_name s =
       let val (qualifier, name) = split_last (Long_Name.explode s)
-      in make_binding ([], map (rpair false) qualifier, name, Position.none) end;
+      in make_binding (false, [], map (rpair false) qualifier, name, Position.none) end;
 
 fun qualified_name_of (b as Binding {qualifier, name, ...}) =
   if is_empty b then ""
@@ -94,13 +101,21 @@
 
 fun prefix_of (Binding {prefix, ...}) = prefix;
 
-fun map_prefix f = map_binding (fn (prefix, qualifier, name, pos) =>
-  (f prefix, qualifier, name, pos));
+fun map_prefix f =
+  map_binding (fn (conceal, prefix, qualifier, name, pos) =>
+    (conceal, f prefix, qualifier, name, pos));
 
 fun prefix _ "" = I
   | prefix mandatory prfx = map_prefix (cons (prfx, mandatory));
 
 
+(* conceal *)
+
+val conceal =
+  map_binding (fn (_, prefix, qualifier, name, pos) =>
+    (true, prefix, qualifier, name, pos));
+
+
 (* str_of *)
 
 fun str_of binding =