# HG changeset patch
# User wenzelm
# Date 1256403897 -7200
# Node ID d23e75d4f7daf8013a56edb781114c4b9e22057b
# Parent  2f05a1feac21b1262caf7df03952f513463b41c6
maintain abstract entry, with position, identity etc.;
declare/define: explicit indication of strictness;
merge_tables/join_tables: disallow duplicates based on entry identity;

diff -r 2f05a1feac21 -r d23e75d4f7da src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Sat Oct 24 18:55:47 2009 +0200
+++ b/src/Pure/General/name_space.ML	Sat Oct 24 19:04:57 2009 +0200
@@ -29,7 +29,7 @@
   val merge: T * T -> T
   type naming
   val default_naming: naming
-  val declare: naming -> binding -> T -> string * T
+  val declare: bool -> naming -> binding -> T -> string * T
   val full_name: naming -> binding -> string
   val external_names: naming -> string -> string list
   val add_path: string -> naming -> naming
@@ -37,11 +37,11 @@
   val parent_path: naming -> naming
   val mandatory_path: string -> naming -> naming
   type 'a table = T * 'a Symtab.table
-  val define: naming -> binding * 'a -> 'a table -> string * 'a table (*exception Symtab.DUP*)
+  val define: bool -> naming -> binding * 'a -> 'a table -> string * 'a table
   val empty_table: 'a table
-  val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table (*exception Symtab.DUP*)
-  val join_tables: (string -> 'a * 'a -> 'a) (*exception Symtab.DUP/Symtab.SAME*) ->
-    'a table * 'a table -> 'a table (*exception Symtab.DUP*)
+  val merge_tables: 'a table * 'a table -> 'a table
+  val join_tables:
+    (string -> 'a * 'a -> 'a) (*Symtab.SAME*) -> 'a table * 'a table -> 'a table
   val dest_table: 'a table -> (string * 'a) list
   val extern_table: 'a table -> (xstring * 'a) list
 end;
@@ -58,12 +58,30 @@
 val is_hidden = String.isPrefix "??.";
 
 
+(* datatype entry *)
+
+type entry =
+ {externals: xstring list,
+  is_system: bool,
+  pos: Position.T,
+  id: serial};
+
+fun make_entry (externals, is_system, pos, id) : entry =
+  {externals = externals, is_system = is_system, pos = pos, id = id};
+
+fun str_of_entry def (name, {pos, id, ...}: entry) =
+  let
+    val occurrence = (if def then Markup.defN else Markup.refN, string_of_int id);
+    val props = occurrence :: Position.properties_of pos;
+  in Markup.markup (Markup.properties props (Markup.entity name)) name end;
+
+
 (* datatype T *)
 
 datatype T =
   NameSpace of
     (string list * string list) Symtab.table *   (*internals, hidden internals*)
-    xstring list Symtab.table;                   (*externals*)
+    entry Symtab.table;
 
 val empty = NameSpace (Symtab.empty, Symtab.empty);
 
@@ -75,16 +93,14 @@
   | SOME (name :: _, _) => (name, false)
   | SOME ([], name' :: _) => (hidden name', true));
 
-fun get_accesses (NameSpace (_, xtab)) name =
-  (case Symtab.lookup xtab name of
+fun get_accesses (NameSpace (_, entries)) name =
+  (case Symtab.lookup entries name of
     NONE => [name]
-  | SOME xnames => xnames);
+  | SOME {externals, ...} => externals);
 
-fun put_accesses name xnames (NameSpace (tab, xtab)) =
-  NameSpace (tab, Symtab.update (name, xnames) xtab);
-
-fun valid_accesses (NameSpace (tab, _)) name = Symtab.fold (fn (xname, (names, _)) =>
-  if not (null names) andalso hd names = name then cons xname else I) tab [];
+fun valid_accesses (NameSpace (tab, _)) name =
+  Symtab.fold (fn (xname, (names, _)) =>
+    if not (null names) andalso hd names = name then cons xname else I) tab [];
 
 
 (* intern and extern *)
@@ -120,8 +136,8 @@
 
 local
 
-fun map_space f xname (NameSpace (tab, xtab)) =
-  NameSpace (Symtab.map_default (xname, ([], [])) f tab, xtab);
+fun map_space f xname (NameSpace (tab, entries)) =
+  NameSpace (Symtab.map_default (xname, ([], [])) f tab, entries);
 
 in
 
@@ -152,17 +168,21 @@
 
 (* merge *)
 
-fun merge (NameSpace (tab1, xtab1), NameSpace (tab2, xtab2)) =
+fun merge (NameSpace (tab1, entries1), NameSpace (tab2, entries2)) =
   let
     val tab' = (tab1, tab2) |> Symtab.join
       (K (fn ((names1, names1'), (names2, names2')) =>
-        if pointer_eq (names1, names2) andalso pointer_eq (names1', names2') then raise Symtab.SAME
+        if pointer_eq (names1, names2) andalso pointer_eq (names1', names2')
+        then raise Symtab.SAME
         else (Library.merge (op =) (names1, names2), Library.merge (op =) (names1', names2'))));
-    val xtab' = (xtab1, xtab2) |> Symtab.join
-      (K (fn xnames =>
-        if pointer_eq xnames then raise Symtab.SAME
-        else (Library.merge (op =) xnames)));
-  in NameSpace (tab', xtab') end;
+    val entries' = (entries1, entries2) |> Symtab.join
+      (fn name => fn (entry1, entry2) =>
+        if #id entry1 = #id entry2 then raise Symtab.SAME
+        else
+          error ("Duplicate declaration " ^
+            quote (str_of_entry true (name, entry1)) ^ " vs. " ^
+            quote (str_of_entry true (name, entry2))));
+  in NameSpace (tab', entries') end;
 
 
 
@@ -225,13 +245,26 @@
 
 (* declaration *)
 
-fun declare naming binding space =
+fun new_entry strict entry (NameSpace (tab, entries)) =
+  let
+    val entries' =
+      (if strict then Symtab.update_new else Symtab.update) entry entries
+        handle Symtab.DUP _ =>
+          error ("Duplicate declaration " ^ quote (str_of_entry true entry));
+  in NameSpace (tab, entries') end;
+
+fun declare strict naming binding space =
   let
     val names = full naming binding;
     val name = Long_Name.implode names;
     val _ = name = "" andalso err_bad binding;
     val (accs, accs') = accesses naming binding;
-    val space' = space |> fold (add_name name) accs |> put_accesses name accs';
+
+    val is_system = false;  (* FIXME *)
+    val entry = make_entry (accs', is_system, Binding.pos_of binding, serial ());
+    val space' = space
+      |> fold (add_name name) accs
+      |> new_entry strict (name, entry);
   in (name, space') end;
 
 
@@ -240,14 +273,14 @@
 
 type 'a table = T * 'a Symtab.table;
 
-fun define naming (binding, x) (space, tab) =
-  let val (name, space') = declare naming binding space
-  in (name, (space', Symtab.update_new (name, x) tab)) end;
+fun define strict naming (binding, x) (space, tab) =
+  let val (name, space') = declare strict naming binding space
+  in (name, (space', Symtab.update (name, x) tab)) end;
 
 val empty_table = (empty, Symtab.empty);
 
-fun merge_tables eq ((space1, tab1), (space2, tab2)) =
-  (merge (space1, space2), Symtab.merge eq (tab1, tab2));
+fun merge_tables ((space1, tab1), (space2, tab2)) =
+  (merge (space1, space2), Symtab.merge (K true) (tab1, tab2));
 
 fun join_tables f ((space1, tab1), (space2, tab2)) =
   (merge (space1, space2), Symtab.join f (tab1, tab2));