tuned storage of code identifiers

--- a/src/Tools/Code/code_namespace.ML	Mon Feb 03 17:55:50 2014 +0100
+++ b/src/Tools/Code/code_namespace.ML	Mon Feb 03 08:23:19 2014 +0100
@@ -42,27 +42,32 @@
 
 (** fundamental module name hierarchy **)
 
-fun lookup_identifier identifiers sym =
-  Code_Symbol.lookup identifiers sym
-  |> Option.map (split_last o Long_Name.explode);
+fun module_fragments' { identifiers, reserved } name =
+  case Code_Symbol.lookup_module_data identifiers name of
+      SOME (fragments, _) => fragments
+    | NONE => map (fn fragment => fst (Name.variant fragment reserved)) (Long_Name.explode name);
+
+fun module_fragments { module_name, identifiers, reserved } =
+  if module_name = ""
+  then module_fragments' { identifiers = identifiers, reserved = reserved }
+  else K (Long_Name.explode module_name);
 
-fun force_identifier ctxt fragments_tab force_module identifiers sym =
-  case lookup_identifier identifiers sym of
-      NONE => ((the o Symtab.lookup fragments_tab o Code_Symbol.default_prefix ctxt) sym, Code_Symbol.default_base sym)
+fun build_module_namespace ctxt { module_prefix, module_name, identifiers, reserved } program =
+  let
+    val module_names = Code_Symbol.Graph.fold (insert (op =) o Code_Symbol.default_prefix ctxt o fst) program [];
+    val module_fragments' = module_fragments
+      { module_name = module_name, identifiers = identifiers, reserved = reserved };
+  in
+    fold (fn name => Symtab.update (name, Long_Name.explode module_prefix @ module_fragments' name))
+      module_names Symtab.empty
+  end;
+
+fun prep_symbol ctxt module_namespace force_module identifiers sym =
+  case Code_Symbol.lookup identifiers sym of
+      NONE => ((the o Symtab.lookup module_namespace o Code_Symbol.default_prefix ctxt) sym, Code_Symbol.default_base sym)
     | SOME prefix_name => if null force_module then prefix_name
         else (force_module, snd prefix_name);
 
-fun build_module_namespace ctxt { module_prefix, module_identifiers, reserved } program =
-  let
-    fun alias_fragments name = case module_identifiers name
-     of SOME name' => Long_Name.explode name'
-      | NONE => map (fn name => fst (Name.variant name reserved)) (Long_Name.explode name);
-    val module_names = Code_Symbol.Graph.fold (insert (op =) o Code_Symbol.default_prefix ctxt o fst) program [];
-  in
-    fold (fn name => Symtab.update (name, Long_Name.explode module_prefix @ alias_fragments name))
-      module_names Symtab.empty
-  end;
-
 
 (** flat program structure **)
 
@@ -73,12 +78,9 @@
   let
 
     (* building module name hierarchy *)
-    val module_identifiers = if module_name = ""
-      then Code_Symbol.lookup_module_data identifiers
-      else K (SOME module_name);
-    val fragments_tab = build_module_namespace ctxt { module_prefix = module_prefix,
-      module_identifiers = module_identifiers, reserved = reserved } program;
-    val prep_sym = force_identifier ctxt fragments_tab (Long_Name.explode module_name) identifiers
+    val module_namespace = build_module_namespace ctxt { module_prefix = module_prefix,
+      module_name = module_name, identifiers = identifiers, reserved = reserved } program;
+    val prep_sym = prep_symbol ctxt module_namespace (Long_Name.explode module_name) identifiers
       #>> Long_Name.implode;
 
     (* distribute statements over hierarchy *)
@@ -165,12 +167,9 @@
   let
 
     (* building module name hierarchy *)
-    val module_identifiers = if module_name = ""
-      then Code_Symbol.lookup_module_data identifiers
-      else K (SOME module_name);
-    val fragments_tab = build_module_namespace ctxt { module_prefix = "",
-      module_identifiers = module_identifiers, reserved = reserved } program;
-    val prep_sym = force_identifier ctxt fragments_tab (Long_Name.explode module_name) identifiers;
+    val module_namespace = build_module_namespace ctxt { module_prefix = "",
+      module_name = module_name, identifiers = identifiers, reserved = reserved } program;
+    val prep_sym = prep_symbol ctxt module_namespace (Long_Name.explode module_name) identifiers;
 
     (* building empty module hierarchy *)
     val empty_module = (empty_data, Code_Symbol.Graph.empty);
@@ -184,9 +183,9 @@
           #> (apsnd o Code_Symbol.Graph.map_node (Code_Symbol.Module name_fragment) o apsnd o map_module_content o allocate_module) name_fragments;
     val empty_program =
       empty_module
-      |> Symtab.fold (fn (_, fragments) => allocate_module fragments) fragments_tab
+      |> Symtab.fold (fn (_, fragments) => allocate_module fragments) module_namespace
       |> Code_Symbol.Graph.fold (allocate_module o these o Option.map fst
-          o lookup_identifier identifiers o fst) program;
+          o Code_Symbol.lookup identifiers o fst) program;
 
     (* distribute statements over hierarchy *)
     fun add_stmt sym stmt =

--- a/src/Tools/Code/code_target.ML	Mon Feb 03 17:55:50 2014 +0100
+++ b/src/Tools/Code/code_target.ML	Mon Feb 03 08:23:19 2014 +0100
@@ -81,7 +81,8 @@
     class * (string * 'c option) list, (class * class) * (string * 'd option) list,
     (class * string) * (string * 'e option) list,
     string * (string * 'f option) list) Code_Symbol.attr;
-type identifier_data = (string, string, string, string, string, string) Code_Symbol.data;
+type identifier_data = (string list * string, string list * string, string list * string, string list * string,
+  string list * string, string list * string) Code_Symbol.data;
 
 type tyco_syntax = Code_Printer.tyco_syntax;
 type raw_const_syntax = Code_Printer.raw_const_syntax;
@@ -144,7 +145,7 @@
           val y' = Name.desymbolize false y;
         in ys' @ [y'] end;
   in if xs' = xs
-    then s
+    then if is_module then (xs, "") else split_last xs
     else error ("Invalid code name: " ^ quote s ^ "\n"
       ^ "better try " ^ quote (Long_Name.implode xs'))
   end;
@@ -372,11 +373,12 @@
     val width = the_default default_width some_width;
   in (fn program => prepared_serializer program width, prepared_program) end;
 
-fun invoke_serializer thy target some_width module_name args program syms =
+fun invoke_serializer thy target some_width raw_module_name args program syms =
   let
-    val check = if module_name = "" then I else check_name true;
+    val module_name = if raw_module_name = "" then ""
+      else (check_name true raw_module_name; raw_module_name)
     val (mounted_serializer, prepared_program) = mount_serializer thy
-      target some_width (check module_name) args program syms;
+      target some_width module_name args program syms;
   in mounted_serializer prepared_program end;
 
 fun assert_module_name "" = error "Empty module name not allowed here"