src/Pure/General/name_space.ML

--- a/src/Pure/General/name_space.ML	Sun Oct 25 19:14:25 2009 +0100
+++ b/src/Pure/General/name_space.ML	Sun Oct 25 19:14:46 2009 +0100
@@ -22,7 +22,8 @@
   type T
   val empty: string -> T
   val kind_of: T -> string
-  val the_entry: T -> string -> {concealed: bool, pos: Position.T, id: serial}
+  val the_entry: T -> string ->
+    {concealed: bool, group: serial option, theory_name: string, pos: Position.T, id: serial}
   val is_concealed: T -> string -> bool
   val intern: T -> xstring -> string
   val extern_flags: {long_names: bool, short_names: bool, unique_names: bool} ->
@@ -32,11 +33,13 @@
   val merge: T * T -> T
   type naming
   val default_naming: naming
+  val conceal: naming -> naming
+  val set_group: serial -> naming -> naming
+  val set_theory_name: string -> naming -> naming
   val add_path: string -> naming -> naming
   val root_path: naming -> naming
   val parent_path: naming -> naming
   val mandatory_path: string -> naming -> naming
-  val conceal: naming -> naming
   val full_name: naming -> binding -> string
   val external_names: naming -> string -> string list
   val declare: bool -> naming -> binding -> T -> string * T
@@ -67,6 +70,8 @@
 type entry =
  {externals: xstring list,
   concealed: bool,
+  group: serial option,
+  theory_name: string,
   pos: Position.T,
   id: serial};
 
@@ -106,7 +111,8 @@
 fun the_entry (Name_Space {kind, entries, ...}) name =
   (case Symtab.lookup entries name of
     NONE => error ("Unknown " ^ kind ^ " " ^ quote name)
-  | SOME {concealed, pos, id, ...} => {concealed = concealed, pos = pos, id = id});
+  | SOME {concealed, group, theory_name, pos, id, ...} =>
+      {concealed = concealed, group = group, theory_name = theory_name, pos = pos, id = id});
 
 fun is_concealed space name = #concealed (the_entry space name);
 
@@ -213,26 +219,44 @@
 
 (* datatype naming *)
 
-datatype naming = Naming of bool * (string * bool) list;
+datatype naming = Naming of
+ {conceal: bool,
+  group: serial option,
+  theory_name: string,
+  path: (string * bool) list};
+
+fun make_naming (conceal, group, theory_name, path) =
+  Naming {conceal = conceal, group = group, theory_name = theory_name, path = path};
+
+fun map_naming f (Naming {conceal, group, theory_name, path}) =
+  make_naming (f (conceal, group, theory_name, path));
 
-fun map_naming f (Naming (conceal, path)) = Naming (f (conceal, path));
-fun map_path f = map_naming (apsnd f);
+fun map_path f = map_naming (fn (conceal, group, theory_name, path) =>
+  (conceal, group, theory_name, f path));
+
+
+val default_naming = make_naming (false, NONE, "", []);
 
-val default_naming = Naming (false, []);
+val conceal = map_naming (fn (_, group, theory_name, path) =>
+  (true, group, theory_name, path));
+
+fun set_group group = map_naming (fn (conceal, _, theory_name, path) =>
+  (conceal, SOME group, theory_name, path));
+
+fun set_theory_name theory_name = map_naming (fn (conceal, group, _, path) =>
+  (conceal, group, theory_name, path));
 
 fun add_path elems = map_path (fn path => path @ [(elems, false)]);
 val root_path = map_path (fn _ => []);
 val parent_path = map_path (perhaps (try (#1 o split_last)));
 fun mandatory_path elems = map_path (fn path => path @ [(elems, true)]);
 
-val conceal = map_naming (fn (_, path) => (true, path));
-
 
 (* full name *)
 
 fun err_bad binding = error ("Bad name binding " ^ quote (Binding.str_of binding));
 
-fun name_spec (Naming (conceal1, path)) binding =
+fun name_spec (Naming {conceal = conceal1, path, ...}) binding =
   let
     val (conceal2, prefix, name) = Binding.dest binding;
     val _ = Long_Name.is_qualified name andalso err_bad binding;
@@ -247,7 +271,7 @@
   in (concealed, if null spec2 then [] else spec) end;
 
 fun full_name naming =
-  name_spec naming #> snd #> map fst #> Long_Name.implode;
+  name_spec naming #> #2 #> map #1 #> Long_Name.implode;
 
 
 (* accesses *)
@@ -284,6 +308,7 @@
 
 fun declare strict naming binding space =
   let
+    val Naming {group, theory_name, ...} = naming;
     val (concealed, spec) = name_spec naming binding;
     val (accs, accs') = accesses naming binding;
 
@@ -293,6 +318,8 @@
     val entry =
      {externals = accs',
       concealed = concealed,
+      group = group,
+      theory_name = theory_name,
       pos = Position.default (Binding.pos_of binding),
       id = serial ()};
     val space' = space |> fold (add_name name) accs |> new_entry strict (name, entry);