# HG changeset patch
# User wenzelm
# Date 1512934274 -3600
# Node ID 35a4bf0f13b3fae0233c05b84e946ad1d4ddccc8
# Parent  70576478bda95f1655b1823e99bfd4850a005c71
clean log file on Windows;

diff -r 70576478bda9 -r 35a4bf0f13b3 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Sun Dec 10 20:29:00 2017 +0100
+++ b/src/Pure/Thy/present.ML	Sun Dec 10 20:31:14 2017 +0100
@@ -196,7 +196,7 @@
     val doc_path = Path.appends [dir, Path.parent, Path.basic name |> Path.ext format];
     val _ = if verbose then writeln script else ();
     val {out, err, rc, ...} = Bash.process script;
-    val _ = if verbose then writeln out else ();
+    val _ = if verbose then writeln (normalize_lines out) else ();
     val _ =
       if not (File.exists doc_path) orelse rc <> 0 then
         cat_error err ("Failed to build document " ^ quote (show_path doc_path))
diff -r 70576478bda9 -r 35a4bf0f13b3 src/Pure/library.ML
--- a/src/Pure/library.ML	Sun Dec 10 20:29:00 2017 +0100
+++ b/src/Pure/library.ML	Sun Dec 10 20:31:14 2017 +0100
@@ -145,6 +145,7 @@
   val unsuffix: string -> string -> string
   val trim_line: string -> string
   val trim_split_lines: string -> string list
+  val normalize_lines: string -> string
   val replicate_string: int -> string -> string
   val translate_string: (string -> string) -> string -> string
   val encode_lines: string -> string
@@ -723,6 +724,11 @@
 
 val trim_split_lines = trim_line #> split_lines #> map trim_line;
 
+fun normalize_lines str =
+  if exists_string (fn s => s = "\r") str then
+    split_lines str |> map trim_line |> cat_lines
+  else str;
+
 fun replicate_string (0: int) _ = ""
   | replicate_string 1 a = a
   | replicate_string k a =