# HG changeset patch
# User wenzelm
# Date 1118311408 -7200
# Node ID e573e5167eda36d28c8ec7b03d4dcd54eddb0f89
# Parent  fd027bb328969f0a509048b79e9b45ee99371ea8
added type NameSpace.table with basic operations;

diff -r fd027bb32896 -r e573e5167eda src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Thu Jun 09 12:03:27 2005 +0200
+++ b/src/Pure/General/name_space.ML	Thu Jun 09 12:03:28 2005 +0200
@@ -3,7 +3,7 @@
     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*)
@@ -37,7 +37,6 @@
   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
@@ -52,6 +51,11 @@
   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 =
@@ -143,9 +147,6 @@
     else ex (accesses' name)
   end;
 
-fun extern_table space tab =
-  Library.sort_wrt #1 (map (apfst (extern space)) (Symtab.dest tab));
-
 
 (* basic operations *)
 
@@ -244,6 +245,23 @@
 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;