# HG changeset patch
# User wenzelm
# Date 1422114157 -3600
# Node ID b65809f05dc9236601a3c2c1720b95ae17528f57
# Parent  f24ac9df7ab21bb8ddfafadd1a060805097903ce
more direct Output.output;
avoid newline in Code_Printer/Pretty.str;

diff -r f24ac9df7ab2 -r b65809f05dc9 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;