src/Pure/General/name_space.ML

--- a/src/Pure/General/name_space.ML	Thu Dec 04 14:44:07 2008 +0100
+++ b/src/Pure/General/name_space.ML	Fri Dec 05 08:04:53 2008 +0100
@@ -33,7 +33,6 @@
   val default_naming: naming
   val declare: naming -> Binding.T -> T -> string * T
   val full_name: naming -> Binding.T -> string
-  val declare_base: naming -> string -> T -> T
   val external_names: naming -> string -> string list
   val path_of: naming -> string
   val add_path: string -> naming -> naming
@@ -45,6 +44,8 @@
   val bind: naming -> Binding.T * 'a
     -> 'a table -> string * 'a table (*exception Symtab.DUP*)
   val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
+  val join_tables: (string -> 'a * 'a -> 'a)
+    -> 'a table * 'a table -> 'a table
   val dest_table: 'a table -> (string * 'a) list
   val extern_table: 'a table -> (xstring * 'a) list
   val extend_table: naming -> (bstring * 'a) list -> 'a table -> 'a table
@@ -264,13 +265,9 @@
 
 (* declarations *)
 
-fun full (Naming (path, (qualify, _))) = qualify path;
+fun full_internal (Naming (path, (qualify, _))) = qualify path;
 
-fun full_name naming b =
-  let val (prefix, bname) = Binding.dest b
-  in full (apply_prefix prefix naming) bname end;
-
-fun declare_base naming name space =
+fun declare_internal naming name space =
   if is_hidden name then
     error ("Attempt to declare hidden name " ^ quote name)
   else
@@ -282,12 +279,16 @@
       val (accs, accs') = pairself (map implode_name) (accesses naming names);
     in space |> fold (add_name name) accs |> put_accesses name accs' end;
 
+fun full_name naming b =
+  let val (prefix, bname) = Binding.dest b
+  in full_internal (apply_prefix prefix naming) bname end;
+
 fun declare bnaming b =
   let
     val (prefix, bname) = Binding.dest b;
     val naming = apply_prefix prefix bnaming;
-    val name = full naming bname;
-  in declare_base naming name #> pair name end;
+    val name = full_internal naming bname;
+  in declare_internal naming name #> pair name end;
 
 
 
@@ -303,12 +304,15 @@
   in (name, (space', Symtab.update_new (name, x) tab)) end;
 
 fun extend_table naming bentries (space, tab) =
-  let val entries = map (apfst (full naming)) bentries
-  in (fold (declare_base naming o #1) entries space, Symtab.extend (tab, entries)) end;
+  let val entries = map (apfst (full_internal naming)) bentries
+  in (fold (declare_internal naming o #1) entries space, Symtab.extend (tab, entries)) end;
 
 fun merge_tables eq ((space1, tab1), (space2, tab2)) =
   (merge (space1, space2), Symtab.merge eq (tab1, tab2));
 
+fun join_tables f ((space1, tab1), (space2, tab2)) =
+  (merge (space1, space2), Symtab.join f (tab1, tab2));
+
 fun ext_table (space, tab) =
   Symtab.fold (fn (name, x) => cons ((name, extern space name), x)) tab []
   |> Library.sort_wrt (#2 o #1);