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 =