# HG changeset patch
# User haftmann
# Date 1378397103 -7200
# Node ID dd64696d267a3a9325ce3a03616b739bfa38e04b
# Parent  ca3fdc640ebf1f1a52b9fae0c7b6e27156660f6e
explicit module names have precedence over identifier declarations

diff -r ca3fdc640ebf -r dd64696d267a src/Tools/Code/code_namespace.ML
--- a/src/Tools/Code/code_namespace.ML	Thu Sep 05 18:05:02 2013 +0200
+++ b/src/Tools/Code/code_namespace.ML	Thu Sep 05 18:05:03 2013 +0200
@@ -48,10 +48,11 @@
   Code_Symbol.lookup identifiers (symbol_of name)
   |> Option.map (split_last o Long_Name.explode);
 
-fun force_identifier symbol_of fragments_tab identifiers name =
+fun force_identifier symbol_of fragments_tab force_module identifiers name =
   case lookup_identifier symbol_of identifiers name of
       NONE => (apfst (the o Symtab.lookup fragments_tab) o split_name) name
-    | SOME name' => name';
+    | SOME prefix_name => if null force_module then prefix_name
+        else (force_module, snd prefix_name);
 
 fun build_module_namespace { module_prefix, module_identifiers, reserved } program =
   let
@@ -79,7 +80,7 @@
       else K (SOME module_name);
     val fragments_tab = build_module_namespace { module_prefix = module_prefix,
       module_identifiers = module_identifiers, reserved = reserved } program;
-    val prep_name = force_identifier symbol_of fragments_tab identifiers
+    val prep_name = force_identifier symbol_of fragments_tab (Long_Name.explode module_name) identifiers
       #>> Long_Name.implode;
 
     (* distribute statements over hierarchy *)
@@ -171,7 +172,7 @@
       else K (SOME module_name);
     val fragments_tab = build_module_namespace { module_prefix = "",
       module_identifiers = module_identifiers, reserved = reserved } program;
-    val prep_name = force_identifier symbol_of fragments_tab identifiers;
+    val prep_name = force_identifier symbol_of fragments_tab (Long_Name.explode module_name) identifiers;
 
     (* building empty module hierarchy *)
     val empty_module = (empty_data, Graph.empty);