more direct Output.output;
authorwenzelm
Sat, 24 Jan 2015 16:42:37 +0100
changeset 59430 b65809f05dc9
parent 59429 f24ac9df7ab2
child 59431 db440f97cf1a
more direct Output.output; avoid newline in Code_Printer/Pretty.str;
src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Sat Jan 24 13:54:19 2015 +0100
+++ b/src/Tools/Code/code_target.ML	Sat Jan 24 16:42:37 2015 +0100
@@ -150,7 +150,7 @@
       string [] width content |> SOME
   | serialization _ string content width (Present syms) =
      string syms width content
-     |> (apfst o map o apsnd) (Pretty.output (SOME width) o Pretty.str)
+     |> (apfst o map o apsnd) Output.output
      |> SOME;
 
 fun export some_path f = (f (Export some_path); ());
@@ -571,7 +571,8 @@
       (arrange check_const_syntax) (arrange check_tyco_syntax)
         (arrange ((K o K o K) I)) (arrange ((K o K o K) I)) (arrange ((K o K o K) I))
         (arrange (fn ctxt => fn _ => fn _ => fn (raw_content, raw_cs) =>
-          (Code_Printer.str raw_content, map (prep_const ctxt) raw_cs)))
+          (Pretty.blk (0, Pretty.fbreaks (map Code_Printer.str (split_lines raw_content))),
+            map (prep_const ctxt) raw_cs)))
   end;
 
 fun cert_printings ctxt = cert_syms ctxt #> arrange_printings cert_const ctxt;