# HG changeset patch
# User haftmann
# Date 1211970288 -7200
# Node ID d21bb9f733640c12b38aa5bfc3d63e09a6cd166e
# Parent  e8a40d8b7897db7d9beb9f92e40d46410e13b2f8
fixed utterly wrong print mode handling

diff -r e8a40d8b7897 -r d21bb9f73364 src/Tools/code/code_package.ML
--- a/src/Tools/code/code_package.ML	Wed May 28 12:06:49 2008 +0200
+++ b/src/Tools/code/code_package.ML	Wed May 28 12:24:48 2008 +0200
@@ -99,7 +99,7 @@
     val code = Program.get thy;
     fun mk_seri_dest file = case file
      of NONE => CodeTarget.compile
-      | SOME "-" => writeln o CodeTarget.string
+      | SOME "-" => CodeTarget.write
       | SOME f => CodeTarget.file (Path.explode f)
     val _ = map (fn (((target, module), file), args) =>
       (mk_seri_dest file (CodeTarget.serialize thy target permissive module args code cs))) seris;
diff -r e8a40d8b7897 -r d21bb9f73364 src/Tools/code/code_target.ML
--- a/src/Tools/code/code_target.ML	Wed May 28 12:06:49 2008 +0200
+++ b/src/Tools/code/code_target.ML	Wed May 28 12:24:48 2008 +0200
@@ -37,6 +37,7 @@
   val serialize: theory -> string -> bool -> string option -> Args.T list
     -> CodeThingol.code -> string list option -> serialization;
   val compile: serialization -> unit;
+  val write: serialization -> unit;
   val file: Path.T -> serialization -> unit;
   val string: serialization -> string;
   val sml_of: theory -> CodeThingol.code -> string list -> string;
@@ -66,7 +67,8 @@
   | enum_default default sep opn cls xs = Pretty.enum sep opn cls xs;
 
 val code_width = ref 80;
-fun code_source p = Pretty.setmp_margin (!code_width) Pretty.string_of p ^ "\n";
+fun code_source p = PrintMode.setmp [] (Pretty.setmp_margin (!code_width) Pretty.string_of) p ^ "\n";
+fun code_writeln p = Pretty.setmp_margin (!code_width) Pretty.writeln p;
 
 
 (** generic syntax **)
@@ -140,10 +142,11 @@
        Symtab.join (K snd) (const1, const2))
   );
 
-datatype serialization_dest = Compile | File of Path.T | String;
+datatype serialization_dest = Compile | Write | File of Path.T | String;
 type serialization = serialization_dest -> string option;
 
 fun compile f = (f Compile; ());
+fun write f = (f Write; ());
 fun file p f = (f (File p); ());
 fun string f = the (f String);
 
@@ -1195,6 +1198,7 @@
     val deresolv = try (deresolver (if is_some module then the_list module else []));
     val output = case seri_dest
      of Compile => K NONE o internal o code_source
+      | Write => K NONE o code_writeln
       | File file => K NONE o File.write file o code_source
       | String => SOME o code_source;
   in output_cont (map_filter deresolv cs, output p) end;
@@ -1567,13 +1571,13 @@
       contr_classparam_typs
       (if string_classes then deriving_show else K false);
     fun assemble_module (modulename, content) =
-      (modulename, code_source (Pretty.chunks [
+      (modulename, Pretty.chunks [
         str ("module " ^ modulename ^ " where {"),
         str "",
         content,
         str "",
         str "}"
-      ]));
+      ]);
     fun seri_module (modlname', (imports, (defs, _))) =
       let
         val imports' =
@@ -1608,11 +1612,12 @@
                 o NameSpace.explode) modlname;
         val pathname = Path.append destination filename;
         val _ = File.mkdir (Path.dir pathname);
-      in File.write pathname content end
+      in File.write pathname (code_source content) end
     val output = case seri_dest
      of Compile => error ("Haskell: no internal compilation")
+      | Write => K NONE o map (code_writeln o snd)
       | File destination => K NONE o map (write_module destination)
-      | String => SOME o cat_lines o map snd;
+      | String => SOME o cat_lines o map (code_source o snd);
   in output (map assemble_module includes
     @ map seri_module (Symtab.dest code'))
   end;