src/Pure/Tools/codegen_serializer.ML

   val mk_flat_ml_resolver: string list -> string -> string;
   val eval_term: string -> string -> string list list
     -> (string -> CodegenThingol.itype pretty_syntax option)
           * (string -> CodegenThingol.iterm pretty_syntax option)
     -> string list
-    -> (string * 'a ref) * CodegenThingol.iterm -> CodegenThingol.module
+    -> (string * 'a option ref) * CodegenThingol.iterm -> CodegenThingol.module
     -> 'a;
   val eval_verbose: bool ref;
   val ml_fun_datatype: string
     -> ((string -> CodegenThingol.itype pretty_syntax option)
         * (string -> CodegenThingol.iterm pretty_syntax option))

       |-> (fn x => pair (Quote x));
     val sym_any = Scan.lift (Scan.one Symbol.not_eof);
     val parse = Scan.repeat (
          (sym "_" -- sym "_" >> K (Arg NOBR))
       || (sym "_" >> K (Arg BR))
-      || (sym "?" >> K Ignore)
       || (sym "/" |-- Scan.repeat (sym " ") >> (Pretty o Pretty.brk o length))
       || Scan.depend (fn ctxt => $$ "{" |-- $$ "*" |-- Scan.repeat1
            (   $$ "'" |-- Scan.one Symbol.not_eof
             || Scan.unless ($$ "*" -- $$ "}") (Scan.one Symbol.not_eof)) --|
          $$ "*" --| $$ "}" >> (implode #> lift_reader ctxt #> swap))

         || pair (parse_nonatomic, BR)
       ) -- OuterParse.string >> (fn ((p, fxy), s) => (p s, fxy));
     fun mk fixity mfx ctxt =
       let
         val i = (length o List.filter is_arg) mfx;
-        val _ = if i > num_args ctxt then error "Too many arguments in codegen syntax" else ();
+        val _ = if i > num_args ctxt then error "Too many arguments in code syntax" else ();
       in (((i, i), fillin_mixfix fixity mfx), ctxt) end;
   in
     parse
     #-> (fn (mfx_reader, fixity) =>
       pair (mfx_reader #-> (fn mfx => mk fixity mfx))

               )
           | from_inst fxy (Context (classes, (v, ~1))) =
               from_lookup BR classes
                 ((str o ml_from_dictvar) v)
           | from_inst fxy (Context (classes, (v, i))) =
-              from_lookup BR (string_of_int (i+1) :: classes)
+              from_lookup BR (classes @ [string_of_int (i+1)])
                 ((str o ml_from_dictvar) v)
       in case lss
        of [] => str "()"
         | [ls] => from_inst fxy ls
         | lss => (Pretty.list "(" ")" o map (from_inst NOBR)) lss

       if is_cons f andalso length es > 1 then
         [(str o resolv) f, Pretty.enum "," "(" ")" (map (ml_from_expr BR) es)]
       else
         (str o resolv) f :: map (ml_from_expr BR) es
     and ml_from_app fxy (app_expr as ((c, (lss, ty)), es)) =
-      case (map (ml_from_insts BR) o filter_out null) lss
+      case if is_cons c then [] else (map (ml_from_insts BR) o filter_out null) lss
        of [] =>
             from_app ml_mk_app ml_from_expr const_syntax fxy app_expr
         | lss =>
             if (is_none o const_syntax) c then
               brackify fxy (

           | mk_cons (co, tys) =
               Pretty.block [
                 str (resolv co),
                 str " of",
                 Pretty.brk 1,
-                Pretty.enum " *" "" "" (map (ml_from_type NOBR) tys)
+                Pretty.enum " *" "" "" (map (ml_from_type (INFX (2, L))) tys)
               ]
         fun mk_datatype definer (t, (vs, cs)) =
           (Pretty.block o Pretty.breaks) (
             str definer
             :: ml_from_tycoexpr NOBR (t, map (ITyVar o fst) vs)

     val serializer = ml_serializer struct_name "ml" nsp_dtcon nspgrp
       (fn "" => (fn p => (use_text Context.ml_output (!eval_verbose) (output p); NONE))
         | _ => SOME) (K NONE, syntax_tyco, syntax_const) (hidden, SOME [NameSpace.pack [nsp_eval, val_name]]);
     val _ = serializer modl';
     val val_name_struct = NameSpace.append struct_name val_name;
-    val _ = use_text Context.ml_output (!eval_verbose) ("val _ = (" ^ ref_name ^ " := " ^ val_name_struct ^ ")");
-    val value = ! reff;
-  in value end;
+    val _ = reff := NONE;
+    val _ = use_text Context.ml_output (!eval_verbose) ("val _ = (" ^ ref_name ^ " := SOME (" ^ val_name_struct ^ "))");
+  in case !reff
+   of NONE => error ("Could not retrieve value of ML reference " ^ quote ref_name
+        ^ " (reference probably has been shadowed)")
+    | SOME value => value
+  end;
 
 fun mk_flat_ml_resolver names =
   let
     val mangler =
       NameMangler.empty

               str "->",
               hs_from_expr NOBR e
             ])
           end
       | hs_from_expr fxy (INum (n, _)) =
-          (str o IntInf.toString) n
+          if n > 0 then
+            (str o IntInf.toString) n
+          else
+            brackify BR [(str o Library.prefix "-" o IntInf.toString o IntInf.~) n]
       | hs_from_expr fxy (IChar (c, _)) =
           (str o enclose "'" "'")
             (let val i = (Char.ord o the o Char.fromString) c
               in if i < 32
                 then Library.prefix "\\" (string_of_int i)