src/Pure/General/name_space.ML

 (*  Title:      Pure/General/name_space.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 Generic name spaces with declared and hidden entries.  Unknown names
-are considered as global; no support for absolute addressing.
+are considered global; no support for absolute addressing.
 *)
 
 type bstring = string;    (*names to be bound / internalized*)
 type xstring = string;    (*externalized names / to be printed*)
 

   type T
   val empty: T
   val valid_accesses: T -> string -> xstring list
   val intern: T -> xstring -> string
   val extern: T -> string -> xstring
-  val extern_table: T -> 'a Symtab.table -> (xstring * 'a) list
   val hide: bool -> string -> T -> T
   val merge: T * T -> T
   val dest: T -> (string * xstring list) list
   type naming
   val path_of: naming -> string

   val qualified_names: naming -> naming
   val no_base_names: naming -> naming
   val custom_accesses: (string list -> string list list) -> naming -> naming
   val set_policy: (string -> bstring -> string) * (string list -> string list list) ->
     naming -> naming
+  type 'a table = T * 'a Symtab.table
+  val empty_table: 'a table
+  val extend_table: naming -> 'a table * (bstring * 'a) list -> 'a table
+  val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
+  val extern_table: 'a table -> (xstring * 'a) list
 end;
 
 structure NameSpace: NAME_SPACE =
 struct
 

   in
     if ! long_names then name
     else if ! short_names then base name
     else ex (accesses' name)
   end;
-
-fun extern_table space tab =
-  Library.sort_wrt #1 (map (apfst (extern space)) (Symtab.dest tab));
 
 
 (* basic operations *)
 
 fun map_space f xname (NameSpace tab) =

 
 fun custom_accesses accs (Naming (path, (qualify, _))) = Naming (path, (qualify, accs));
 fun set_policy policy (Naming (path, _)) = Naming (path, policy);
 
 
+
+(** name spaces coupled with symbol tables **)
+
+type 'a table = T * 'a Symtab.table;
+
+val empty_table = (empty, Symtab.empty);
+
+fun extend_table naming ((space, tab), bentries) =
+  let val entries = map (apfst (full naming)) bentries
+  in (fold (declare 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 extern_table (space, tab) =
+  Library.sort_wrt #1 (map (apfst (extern space)) (Symtab.dest tab));
+
 end;
 
 structure BasicNameSpace: BASIC_NAME_SPACE = NameSpace;
 open BasicNameSpace;