# HG changeset patch
# User wenzelm
# Date 1256410448 -7200
# Node ID db3c18fd9708bba2fe1a588f8f21068ce4c76ad2
# Parent  bbd52d2f869600c684ab27d43b192f83825bfd1e
maintain explicit name space kind;
export Name_Space.the_entry;
tuned messages;

diff -r bbd52d2f8696 -r db3c18fd9708 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Sat Oct 24 19:47:37 2009 +0200
+++ b/src/Pure/General/name_space.ML	Sat Oct 24 20:54:08 2009 +0200
@@ -20,7 +20,9 @@
   val hidden: string -> string
   val is_hidden: string -> bool
   type T
-  val empty: T
+  val empty: string -> T
+  val kind_of: T -> string
+  val the_entry: T -> string -> {is_system: bool, pos: Position.T, id: serial}
   val intern: T -> xstring -> string
   val extern: T -> string -> xstring
   val extern_flags: {long_names: bool, short_names: bool, unique_names: bool} ->
@@ -38,7 +40,7 @@
   val mandatory_path: string -> naming -> naming
   type 'a table = T * 'a Symtab.table
   val define: bool -> naming -> binding * 'a -> 'a table -> string * 'a table
-  val empty_table: 'a table
+  val empty_table: string -> 'a table
   val merge_tables: 'a table * 'a table -> 'a table
   val join_tables:
     (string -> 'a * 'a -> 'a) (*Symtab.SAME*) -> 'a table * 'a table -> 'a table
@@ -66,41 +68,63 @@
   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;
 
+fun err_dup kind entry1 entry2 =
+  error ("Duplicate " ^ kind ^ " declaration " ^
+    quote (str_of_entry true entry1) ^ " vs. " ^ quote (str_of_entry true entry2));
+
 
 (* datatype T *)
 
 datatype T =
   Name_Space of
-    (string list * string list) Symtab.table *   (*internals, hidden internals*)
-    entry Symtab.table;
+   {kind: string,
+    internals: (string list * string list) Symtab.table,  (*visible, hidden*)
+    entries: entry Symtab.table};
+
+fun make_name_space (kind, internals, entries) =
+  Name_Space {kind = kind, internals = internals, entries = entries};
+
+fun map_name_space f (Name_Space {kind = kind, internals = internals, entries = entries}) =
+  make_name_space (f (kind, internals, entries));
+
+fun map_internals f xname = map_name_space (fn (kind, internals, entries) =>
+  (kind, Symtab.map_default (xname, ([], [])) f internals, entries));
+
 
-val empty = Name_Space (Symtab.empty, Symtab.empty);
+fun empty kind = make_name_space (kind, Symtab.empty, Symtab.empty);
+
+fun kind_of (Name_Space {kind, ...}) = kind;
 
-fun lookup (Name_Space (tab, _)) xname =
-  (case Symtab.lookup tab xname of
+fun the_entry (Name_Space {kind, entries, ...}) name =
+  (case Symtab.lookup entries name of
+    NONE => error ("Unknown " ^ kind ^ " " ^ quote name)
+  | SOME {is_system, pos, id, ...} => {is_system = is_system, pos = pos, id = id});
+
+
+(* name accesses *)
+
+fun lookup (Name_Space {internals, ...}) xname =
+  (case Symtab.lookup internals xname of
     NONE => (xname, true)
   | SOME ([], []) => (xname, true)
   | SOME ([name], _) => (name, true)
   | SOME (name :: _, _) => (name, false)
   | SOME ([], name' :: _) => (hidden name', true));
 
-fun get_accesses (Name_Space (_, entries)) name =
+fun get_accesses (Name_Space {entries, ...}) name =
   (case Symtab.lookup entries name of
     NONE => [name]
   | SOME {externals, ...} => externals);
 
-fun valid_accesses (Name_Space (tab, _)) name =
+fun valid_accesses (Name_Space {internals, ...}) name =
   Symtab.fold (fn (xname, (names, _)) =>
-    if not (null names) andalso hd names = name then cons xname else I) tab [];
+    if not (null names) andalso hd names = name then cons xname else I) internals [];
 
 
 (* intern and extern *)
@@ -132,21 +156,13 @@
     unique_names = ! unique_names} space name;
 
 
-(* basic operations *)
-
-local
-
-fun map_space f xname (Name_Space (tab, entries)) =
-  Name_Space (Symtab.map_default (xname, ([], [])) f tab, entries);
+(* modify internals *)
 
-in
-
-val del_name = map_space o apfst o remove (op =);
-fun del_name_extra name = map_space (apfst (fn [] => [] | x :: xs => x :: remove (op =) name xs));
-val add_name = map_space o apfst o update (op =);
-val add_name' = map_space o apsnd o update (op =);
-
-end;
+val del_name = map_internals o apfst o remove (op =);
+fun del_name_extra name =
+  map_internals (apfst (fn [] => [] | x :: xs => x :: remove (op =) name xs));
+val add_name = map_internals o apfst o update (op =);
+val add_name' = map_internals o apsnd o update (op =);
 
 
 (* hide *)
@@ -168,9 +184,15 @@
 
 (* merge *)
 
-fun merge (Name_Space (tab1, entries1), Name_Space (tab2, entries2)) =
+fun merge
+  (Name_Space {kind = kind1, internals = internals1, entries = entries1},
+    Name_Space {kind = kind2, internals = internals2, entries = entries2}) =
   let
-    val tab' = (tab1, tab2) |> Symtab.join
+    val kind' =
+      if kind1 = kind2 then kind1
+      else error ("Attempt to merge different kinds of name spaces " ^
+        quote kind1 ^ " vs. " ^ quote kind2);
+    val internals' = (internals1, internals2) |> Symtab.join
       (K (fn ((names1, names1'), (names2, names2')) =>
         if pointer_eq (names1, names2) andalso pointer_eq (names1', names2')
         then raise Symtab.SAME
@@ -178,11 +200,8 @@
     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 Name_Space (tab', entries') end;
+        else err_dup kind' (name, entry1) (name, entry2));
+  in make_name_space (kind', internals', entries') end;
 
 
 
@@ -245,13 +264,14 @@
 
 (* declaration *)
 
-fun new_entry strict entry (Name_Space (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 Name_Space (tab, entries') end;
+fun new_entry strict entry =
+  map_name_space (fn (kind, internals, entries) =>
+    let
+      val entries' =
+        (if strict then Symtab.update_new else Symtab.update) entry entries
+          handle Symtab.DUP dup =>
+            err_dup kind (dup, the (Symtab.lookup entries dup)) entry;
+    in (kind, internals, entries') end);
 
 fun declare strict naming binding space =
   let
@@ -259,12 +279,12 @@
     val name = Long_Name.implode names;
     val _ = name = "" andalso err_bad binding;
     val (accs, accs') = accesses naming binding;
-
-    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);
+    val entry =
+     {externals = accs',
+      is_system = false,
+      pos = Binding.pos_of binding,
+      id = serial ()};
+    val space' = space |> fold (add_name name) accs |> new_entry strict (name, entry);
   in (name, space') end;
 
 
@@ -277,7 +297,7 @@
   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 empty_table kind = (empty kind, Symtab.empty);
 
 fun merge_tables ((space1, tab1), (space2, tab2)) =
   (merge (space1, space2), Symtab.merge (K true) (tab1, tab2));
diff -r bbd52d2f8696 -r db3c18fd9708 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sat Oct 24 19:47:37 2009 +0200
+++ b/src/Pure/Isar/attrib.ML	Sat Oct 24 20:54:08 2009 +0200
@@ -68,7 +68,7 @@
 structure Attributes = TheoryDataFun
 (
   type T = ((src -> attribute) * string) Name_Space.table;
-  val empty = Name_Space.empty_table;
+  val empty = Name_Space.empty_table "attribute";
   val copy = I;
   val extend = I;
   fun merge _ tables : T = Name_Space.merge_tables tables;
diff -r bbd52d2f8696 -r db3c18fd9708 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sat Oct 24 19:47:37 2009 +0200
+++ b/src/Pure/Isar/locale.ML	Sat Oct 24 20:54:08 2009 +0200
@@ -125,7 +125,7 @@
 structure Locales = TheoryDataFun
 (
   type T = locale Name_Space.table;
-  val empty = Name_Space.empty_table;
+  val empty = Name_Space.empty_table "locale";
   val copy = I;
   val extend = I;
   fun merge _ = Name_Space.join_tables (K merge_locale);
diff -r bbd52d2f8696 -r db3c18fd9708 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Sat Oct 24 19:47:37 2009 +0200
+++ b/src/Pure/Isar/method.ML	Sat Oct 24 20:54:08 2009 +0200
@@ -323,7 +323,7 @@
 structure Methods = TheoryDataFun
 (
   type T = ((src -> Proof.context -> method) * string) Name_Space.table;
-  val empty = Name_Space.empty_table;
+  val empty = Name_Space.empty_table "method";
   val copy = I;
   val extend = I;
   fun merge _ tables : T = Name_Space.merge_tables tables;
diff -r bbd52d2f8696 -r db3c18fd9708 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Sat Oct 24 19:47:37 2009 +0200
+++ b/src/Pure/consts.ML	Sat Oct 24 20:54:08 2009 +0200
@@ -29,7 +29,7 @@
   val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
   val typargs: T -> string * typ -> typ list
   val instance: T -> string * typ list -> typ
-  val declare: bool -> Name_Space.naming -> Properties.T -> (binding * typ) -> T -> T
+  val declare: bool -> Name_Space.naming -> Properties.T -> binding * typ -> T -> T
   val constrain: string * typ option -> T -> T
   val abbreviate: Pretty.pp -> Type.tsig -> Name_Space.naming -> string -> Properties.T ->
     binding * term -> T -> (term * term) * T
@@ -307,7 +307,7 @@
 
 (* empty and merge *)
 
-val empty = make_consts (Name_Space.empty_table, Symtab.empty, Symtab.empty);
+val empty = make_consts (Name_Space.empty_table "constant", Symtab.empty, Symtab.empty);
 
 fun merge
    (Consts {decls = decls1, constraints = constraints1, rev_abbrevs = rev_abbrevs1},
diff -r bbd52d2f8696 -r db3c18fd9708 src/Pure/facts.ML
--- a/src/Pure/facts.ML	Sat Oct 24 19:47:37 2009 +0200
+++ b/src/Pure/facts.ML	Sat Oct 24 20:54:08 2009 +0200
@@ -126,7 +126,7 @@
   props: thm Net.net};
 
 fun make_facts facts props = Facts {facts = facts, props = props};
-val empty = make_facts Name_Space.empty_table Net.empty;
+val empty = make_facts (Name_Space.empty_table "fact") Net.empty;
 
 
 (* named facts *)
diff -r bbd52d2f8696 -r db3c18fd9708 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Sat Oct 24 19:47:37 2009 +0200
+++ b/src/Pure/simplifier.ML	Sat Oct 24 20:54:08 2009 +0200
@@ -148,7 +148,7 @@
 structure Simprocs = GenericDataFun
 (
   type T = simproc Name_Space.table;
-  val empty = Name_Space.empty_table;
+  val empty = Name_Space.empty_table "simproc";
   val extend = I;
   fun merge _ simprocs = Name_Space.merge_tables simprocs;
 );
diff -r bbd52d2f8696 -r db3c18fd9708 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Sat Oct 24 19:47:37 2009 +0200
+++ b/src/Pure/theory.ML	Sat Oct 24 20:54:08 2009 +0200
@@ -89,18 +89,18 @@
 structure ThyData = TheoryDataFun
 (
   type T = thy;
-  val empty = make_thy (Name_Space.empty_table, Defs.empty, ([], []));
+  val empty_axioms = Name_Space.empty_table "axiom";
+  val empty = make_thy (empty_axioms, Defs.empty, ([], []));
   val copy = I;
 
-  fun extend (Thy {axioms = _, defs, wrappers}) =
-    make_thy (Name_Space.empty_table, defs, wrappers);
+  fun extend (Thy {axioms = _, defs, wrappers}) = make_thy (empty_axioms, defs, wrappers);
 
   fun merge pp (thy1, thy2) =
     let
       val Thy {axioms = _, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
       val Thy {axioms = _, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
 
-      val axioms' = Name_Space.empty_table;
+      val axioms' = empty_axioms;
       val defs' = Defs.merge pp (defs1, defs2);
       val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
       val ens' = Library.merge (eq_snd op =) (ens1, ens2);
diff -r bbd52d2f8696 -r db3c18fd9708 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Oct 24 19:47:37 2009 +0200
+++ b/src/Pure/thm.ML	Sat Oct 24 20:54:08 2009 +0200
@@ -1727,7 +1727,7 @@
 structure Oracles = TheoryDataFun
 (
   type T = unit Name_Space.table;
-  val empty = Name_Space.empty_table;
+  val empty = Name_Space.empty_table "oracle";
   val copy = I;
   val extend = I;
   fun merge _ oracles : T = Name_Space.merge_tables oracles;
diff -r bbd52d2f8696 -r db3c18fd9708 src/Pure/type.ML
--- a/src/Pure/type.ML	Sat Oct 24 19:47:37 2009 +0200
+++ b/src/Pure/type.ML	Sat Oct 24 20:54:08 2009 +0200
@@ -120,7 +120,7 @@
   build_tsig (f (classes, default, types));
 
 val empty_tsig =
-  build_tsig ((Name_Space.empty, Sorts.empty_algebra), [], Name_Space.empty_table);
+  build_tsig ((Name_Space.empty "class", Sorts.empty_algebra), [], Name_Space.empty_table "type");
 
 
 (* classes and sorts *)