1.1 --- a/src/Tools/code/code_target.ML	Wed May 28 12:06:49 2008 +0200
     1.2 +++ b/src/Tools/code/code_target.ML	Wed May 28 12:24:48 2008 +0200
     1.3 @@ -37,6 +37,7 @@
     1.4    val serialize: theory -> string -> bool -> string option -> Args.T list
     1.5      -> CodeThingol.code -> string list option -> serialization;
     1.6    val compile: serialization -> unit;
     1.7 +  val write: serialization -> unit;
     1.8    val file: Path.T -> serialization -> unit;
     1.9    val string: serialization -> string;
    1.10    val sml_of: theory -> CodeThingol.code -> string list -> string;
    1.11 @@ -66,7 +67,8 @@
    1.12    | enum_default default sep opn cls xs = Pretty.enum sep opn cls xs;
    1.13  
    1.14  val code_width = ref 80;
    1.15 -fun code_source p = Pretty.setmp_margin (!code_width) Pretty.string_of p ^ "\n";
    1.16 +fun code_source p = PrintMode.setmp [] (Pretty.setmp_margin (!code_width) Pretty.string_of) p ^ "\n";
    1.17 +fun code_writeln p = Pretty.setmp_margin (!code_width) Pretty.writeln p;
    1.18  
    1.19  
    1.20  (** generic syntax **)
    1.21 @@ -140,10 +142,11 @@
    1.22         Symtab.join (K snd) (const1, const2))
    1.23    );
    1.24  
    1.25 -datatype serialization_dest = Compile | File of Path.T | String;
    1.26 +datatype serialization_dest = Compile | Write | File of Path.T | String;
    1.27  type serialization = serialization_dest -> string option;
    1.28  
    1.29  fun compile f = (f Compile; ());
    1.30 +fun write f = (f Write; ());
    1.31  fun file p f = (f (File p); ());
    1.32  fun string f = the (f String);
    1.33  
    1.34 @@ -1195,6 +1198,7 @@
    1.35      val deresolv = try (deresolver (if is_some module then the_list module else []));
    1.36      val output = case seri_dest
    1.37       of Compile => K NONE o internal o code_source
    1.38 +      | Write => K NONE o code_writeln
    1.39        | File file => K NONE o File.write file o code_source
    1.40        | String => SOME o code_source;
    1.41    in output_cont (map_filter deresolv cs, output p) end;
    1.42 @@ -1567,13 +1571,13 @@
    1.43        contr_classparam_typs
    1.44        (if string_classes then deriving_show else K false);
    1.45      fun assemble_module (modulename, content) =
    1.46 -      (modulename, code_source (Pretty.chunks [
    1.47 +      (modulename, Pretty.chunks [
    1.48          str ("module " ^ modulename ^ " where {"),
    1.49          str "",
    1.50          content,
    1.51          str "",
    1.52          str "}"
    1.53 -      ]));
    1.54 +      ]);
    1.55      fun seri_module (modlname', (imports, (defs, _))) =
    1.56        let
    1.57          val imports' =
    1.58 @@ -1608,11 +1612,12 @@
    1.59                  o NameSpace.explode) modlname;
    1.60          val pathname = Path.append destination filename;
    1.61          val _ = File.mkdir (Path.dir pathname);
    1.62 -      in File.write pathname content end
    1.63 +      in File.write pathname (code_source content) end
    1.64      val output = case seri_dest
    1.65       of Compile => error ("Haskell: no internal compilation")
    1.66 +      | Write => K NONE o map (code_writeln o snd)
    1.67        | File destination => K NONE o map (write_module destination)
    1.68 -      | String => SOME o cat_lines o map snd;
    1.69 +      | String => SOME o cat_lines o map (code_source o snd);
    1.70    in output (map assemble_module includes
    1.71      @ map seri_module (Symtab.dest code'))
    1.72    end;