code generation: explicitly declared identifiers gain predence over implicit ones

--- a/src/Doc/IsarRef/HOL_Specific.thy	Mon Feb 03 08:23:20 2014 +0100
+++ b/src/Doc/IsarRef/HOL_Specific.thy	Mon Feb 03 08:23:21 2014 +0100
@@ -2640,9 +2640,11 @@
   \item @{command (HOL) "code_identifier"} associates a a series of symbols
   (constants, type constructors, classes, class relations, instances,
   module names) with target-specific hints how these symbols shall be named.
-  \emph{Warning:} These hints are still subject to name disambiguation.
+  These hints gain precedence over names for symbols with no hints at all.
+  Conflicting hints are subject to name disambiguation.
   @{command (HOL) "code_modulename"} is a legacy variant for
-  @{command (HOL) "code_identifier"} on module names.  It is at the discretion
+  @{command (HOL) "code_identifier"} on module names.
+  \emph{Warning:} It is at the discretion
   of the user to ensure that name prefixes of identifiers in compound
   statements like type classes or datatypes are still the same.
 

--- a/src/Tools/Code/code_namespace.ML	Mon Feb 03 08:23:20 2014 +0100
+++ b/src/Tools/Code/code_namespace.ML	Mon Feb 03 08:23:21 2014 +0100
@@ -69,12 +69,16 @@
     | SOME prefix_name => if null force_module then prefix_name
         else (force_module, snd prefix_name);
 
+fun has_priority identifiers = is_some o Code_Symbol.lookup identifiers;
+
 fun build_proto_program { empty, add_stmt, add_dep } program =
   empty
   |> Code_Symbol.Graph.fold (fn (sym, (stmt, _)) => add_stmt sym stmt) program
   |> Code_Symbol.Graph.fold (fn (sym, (_, (_, syms))) =>
       Code_Symbol.Graph.Keys.fold (add_dep sym) syms) program;
 
+fun prioritize has_priority = uncurry append o List.partition has_priority;
+
 
 (** flat program structure **)
 
@@ -90,6 +94,7 @@
     val prep_sym = prep_symbol ctxt { module_namespace = module_namespace,
       force_module = Long_Name.explode module_name, identifiers = identifiers }
       #>> Long_Name.implode;
+    val sym_priority = has_priority identifiers;
 
     (* distribute statements over hierarchy *)
     fun add_stmt sym stmt =
@@ -117,7 +122,8 @@
         val gr' = (Code_Symbol.Graph.map_node sym o apfst) (K base') gr;
       in (gr', nsp') end;
     fun declarations gr = (gr, empty_nsp)
-      |> fold (fn sym => declare sym (Code_Symbol.Graph.get_node gr sym)) (Code_Symbol.Graph.keys gr) 
+      |> fold (fn sym => declare sym (Code_Symbol.Graph.get_node gr sym))
+          (prioritize sym_priority (Code_Symbol.Graph.keys gr))
       |> fst
       |> (Code_Symbol.Graph.map o K o apsnd) modify_stmt;
     val flat_program = proto_program
@@ -176,7 +182,8 @@
     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 = module_namespace,
-      force_module = Long_Name.explode module_name, identifiers = identifiers };
+      force_module = Long_Name.explode module_name, identifiers = identifiers }
+    val sym_priority = has_priority identifiers;
 
     (* building empty module hierarchy *)
     val empty_module = (empty_data, Code_Symbol.Graph.empty);
@@ -223,9 +230,12 @@
     (* name declarations, data and statement modifications *)
     fun make_declarations nsps (data, nodes) =
       let
-        val (module_fragments, stmt_syms) = List.partition
-          (fn sym => case Code_Symbol.Graph.get_node nodes sym
-            of (_, Module _) => true | _ => false) (Code_Symbol.Graph.keys nodes);
+        val (module_fragments, stmt_syms) =
+          Code_Symbol.Graph.keys nodes
+          |> List.partition
+              (fn sym => case Code_Symbol.Graph.get_node nodes sym
+                of (_, Module _) => true | _ => false)
+          |> pairself (prioritize sym_priority)
         fun declare namify sym (nsps, nodes) =
           let
             val (base, node) = Code_Symbol.Graph.get_node nodes sym;