src/Pure/Tools/codegen_serializer.ML

 
 structure CodegenSerializer: CODEGEN_SERIALIZER =
 struct
 
 open BasicCodegenThingol;
-val debug_msg = CodegenThingol.debug_msg;
+val tracing = CodegenThingol.tracing;
 
 (** precedences **)
 
 datatype lrx = L | R | X;
 

     fun from_module' resolv imps ((name_qual, name), defs) =
       from_module resolv imps ((name_qual, name), defs)
       |> postprocess (resolv name_qual);
   in
     code
-    |> debug_msg (fn _ => "dropping shadowed defintions...")
+    |> tracing (fn _ => "dropping shadowed defintions...")
     |> CodegenThingol.delete_garbage drop
-    |> debug_msg (fn _ => "projecting...")
+    |> tracing (fn _ => "projecting...")
     |> (if is_some select then (CodegenThingol.project_module o the) select else I)
-    |> debug_msg (fn _ => "serializing...")
+    |> tracing (fn _ => "serializing...")
     |> CodegenThingol.serialize (from_defs (class_syntax, tyco_syntax, const_syntax))
          from_module' validator postproc nspgrp name_root
     |> K ()
   end;
 

     fun first_upper s =
       implode (nth_map 0 (Symbol.to_ascii_upper) (explode s));
     fun ml_from_dictvar v = 
       first_upper v ^ "_";
     val ml_from_label =
-      str o translate_string (fn "_" => "__" | "." => "_" | c => c)
-        o NameSpace.base o resolv;
+      str o translate_string (fn "." => "__" | c => c);
     fun ml_from_tyvar (v, []) =
           str "()"
       | ml_from_tyvar (v, sort) =
           let
             fun mk_class class =

         )
       end;
   in (ml_from_funs, ml_from_datatypes) end;
 
 fun ml_from_defs init_ctxt
-    (_, tyco_syntax, const_syntax) resolver prefix defs =
-  let
-    val resolv = resolver prefix;
+    (_, tyco_syntax, const_syntax) resolver prefx defs =
+  let
+    val resolv = resolver prefx;
     val (ml_from_dictvar, ml_from_label, ml_from_tyvar, ml_from_insts, ml_from_tycoexpr, ml_from_type, ml_from_expr) =
       ml_expr_seri (tyco_syntax, const_syntax) resolv;
     val (ml_from_funs, ml_from_datatypes) =
       ml_fun_datatype init_ctxt (tyco_syntax, const_syntax) resolv;
     val filter_datatype =

             Pretty.brk 1,
             (str o resolv) class
           ];
         fun from_membr (m, ty) =
           Pretty.block [
-            ml_from_label m,
+            (ml_from_label o suffix "_" o NameSpace.base) m,
             str ":",
             Pretty.brk 1,
             ml_from_type NOBR ty
           ];
         fun from_membr_fun (m, _) =
           (Pretty.block o Pretty.breaks) [
             str "fun",
             (str o resolv) m,
             Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ resolv name)],
             str "=",
-            Pretty.block [str "#", ml_from_label m],
+            Pretty.block [str "#", (ml_from_label o suffix "_" o NameSpace.base) m],
             str (w ^ ";")
           ];
       in
         Pretty.chunks (
           (Pretty.block o Pretty.breaks) [

                     then NONE else (SOME o NameSpace.base o resolv) c) (CodegenThingol.add_constnames e []);
                 val var_ctxt = init_ctxt
                   |> intro_ctxt consts;
               in
                 (Pretty.block o Pretty.breaks) [
-                  ml_from_label m,
+                  (ml_from_label o suffix "_" o NameSpace.base) m,
                   str "=",
                   ml_from_expr var_ctxt NOBR e
                 ]
               end;
             fun mk_corp rhs =

                   hs_from_expr var_ctxt' NOBR se,
                   str "->",
                   hs_from_expr var_ctxt' NOBR be
                 ]
               end
-          in Pretty.block [
+          in Pretty.enclose "(" ")" [
             str "case",
             Pretty.brk 1,
             hs_from_expr var_ctxt NOBR de,
             Pretty.brk 1,
             str "of",

           in
             (Pretty.block o Pretty.breaks) [
               str "data",
               hs_from_typparms_tycoexpr tyvar_ctxt (vs, (resolv_here name, map (ITyVar o fst) vs)),
               str "=",
-              Pretty.block (separate (Pretty.block [Pretty.brk 1, str "| "]) (map mk_cons constrs))
+              Pretty.block (separate (Pretty.block [Pretty.fbrk, str "| "]) (map mk_cons constrs))
             ]
           end |> SOME
       | hs_from_def (_, CodegenThingol.Datatypecons _) =
           NONE
       | hs_from_def (name, CodegenThingol.Class (supclasss, (v, membrs))) =