clean log file on Windows;
authorwenzelm
Sun Dec 10 20:31:14 2017 +0100 (17 months ago)
changeset 6717935a4bf0f13b3
parent 67178 70576478bda9
child 67180 dcac4659d482
clean log file on Windows;
src/Pure/Thy/present.ML
src/Pure/library.ML
     1.1 --- a/src/Pure/Thy/present.ML	Sun Dec 10 20:29:00 2017 +0100
     1.2 +++ b/src/Pure/Thy/present.ML	Sun Dec 10 20:31:14 2017 +0100
     1.3 @@ -196,7 +196,7 @@
     1.4      val doc_path = Path.appends [dir, Path.parent, Path.basic name |> Path.ext format];
     1.5      val _ = if verbose then writeln script else ();
     1.6      val {out, err, rc, ...} = Bash.process script;
     1.7 -    val _ = if verbose then writeln out else ();
     1.8 +    val _ = if verbose then writeln (normalize_lines out) else ();
     1.9      val _ =
    1.10        if not (File.exists doc_path) orelse rc <> 0 then
    1.11          cat_error err ("Failed to build document " ^ quote (show_path doc_path))
     2.1 --- a/src/Pure/library.ML	Sun Dec 10 20:29:00 2017 +0100
     2.2 +++ b/src/Pure/library.ML	Sun Dec 10 20:31:14 2017 +0100
     2.3 @@ -145,6 +145,7 @@
     2.4    val unsuffix: string -> string -> string
     2.5    val trim_line: string -> string
     2.6    val trim_split_lines: string -> string list
     2.7 +  val normalize_lines: string -> string
     2.8    val replicate_string: int -> string -> string
     2.9    val translate_string: (string -> string) -> string -> string
    2.10    val encode_lines: string -> string
    2.11 @@ -723,6 +724,11 @@
    2.12  
    2.13  val trim_split_lines = trim_line #> split_lines #> map trim_line;
    2.14  
    2.15 +fun normalize_lines str =
    2.16 +  if exists_string (fn s => s = "\r") str then
    2.17 +    split_lines str |> map trim_line |> cat_lines
    2.18 +  else str;
    2.19 +
    2.20  fun replicate_string (0: int) _ = ""
    2.21    | replicate_string 1 a = a
    2.22    | replicate_string k a =