src/Pure/Tools/codegen_serializer.ML
changeset 18361 3126d01e9e35
parent 18360 a2c9506b62a7
child 18380 9668764224a7
--- a/src/Pure/Tools/codegen_serializer.ML	Tue Dec 06 16:07:25 2005 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML	Tue Dec 06 17:11:40 2005 +0100
@@ -644,7 +644,7 @@
     |> eliminate_classes
     |> debug 3 (fn _ => "generating...")
     |> serialize (ml_from_defs tyco_syntax const_syntax) ml_from_module ml_validator nspgrp name_root
-    |> (fn p => Pretty.chunks [(Pretty.str o mk_prims) prims, p])
+    |> (fn p => Pretty.chunks [setmp print_mode [] (Pretty.str o mk_prims) prims, p])
   end;
 
 fun ml_from_thingol' nspgrp name_root =
@@ -664,8 +664,6 @@
 
 local
 
-val bslash = "\\";
-
 fun haskell_from_defs tyco_syntax const_syntax is_cons resolv defs =
   let
     val resolv = fn s =>
@@ -822,7 +820,7 @@
             val (vs, body) = unfold_abs e
           in
             brackify (eval_br br BR) (
-              Pretty.str bslash
+              Pretty.str "\\"
               :: map (Pretty.str o lower_first o fst) vs @ [
               Pretty.str "->",
               haskell_from_expr NOBR body
@@ -958,7 +956,6 @@
       end;
     fun haskell_from_classes defs =
       let
-        val _ = writeln ("IDS: " ^ (commas o map fst) defs)
         fun mk_member (f, ty) =
           Pretty.block [
             Pretty.str (f ^ " ::"),
@@ -1092,7 +1089,7 @@
     |> eta_expand eta_expander
     |> debug 3 (fn _ => "generating...")
     |> serialize (haskell_from_defs tyco_syntax const_syntax is_cons) haskell_from_module haskell_validator nspgrp name_root
-    |> (fn p => Pretty.chunks [(Pretty.str o mk_prims) prims, p])
+    |> (fn p => Pretty.chunks [setmp print_mode [] (Pretty.str o mk_prims) prims, p])
   end;
 
 end; (* local *)