# HG changeset patch
# User wenzelm
# Date 1495474972 -7200
# Node ID 8411f1a2272c487b0f159e8df658ac3720265c2e
# Parent  692e428803c8ff69ed448cd68be118bde687396c
permissive trim_line as in Scala, e.g. relevant for poly/TextIO.print output on Windows;

diff -r 692e428803c8 -r 8411f1a2272c src/HOL/Library/code_test.ML
--- a/src/HOL/Library/code_test.ML	Mon May 22 19:34:01 2017 +0200
+++ b/src/HOL/Library/code_test.ML	Mon May 22 19:42:52 2017 +0200
@@ -119,7 +119,7 @@
 fun parse_result target out =
   (case split_first_last start_markerN end_markerN out of
     NONE => error ("Evaluation failed for " ^ target ^ "!\nBash output:\n" ^ out)
-  | SOME (_, middle, _) => middle |> trim_line |> split_lines |> map parse_line)
+  | SOME (_, middle, _) => middle |> trim_split_lines |> map parse_line)
 
 
 (* pretty printing of test results *)
diff -r 692e428803c8 -r 8411f1a2272c src/Pure/library.ML
--- a/src/Pure/library.ML	Mon May 22 19:34:01 2017 +0200
+++ b/src/Pure/library.ML	Mon May 22 19:42:52 2017 +0200
@@ -144,6 +144,7 @@
   val unprefix: string -> string -> string
   val unsuffix: string -> string -> string
   val trim_line: string -> string
+  val trim_split_lines: string -> string list
   val replicate_string: int -> string -> string
   val translate_string: (string -> string) -> string -> string
   val align_right: string -> int -> string -> string
@@ -711,7 +712,14 @@
   if String.isSuffix sffx s then String.substring (s, 0, size s - size sffx)
   else raise Fail "unsuffix";
 
-val trim_line = perhaps (try (unsuffix "\n"));
+fun trim_line s =
+  if String.isSuffix "\r\n" s
+  then String.substring (s, 0, size s - 2)
+  else if String.isSuffix "\r" s orelse String.isSuffix "\n" s
+  then String.substring (s, 0, size s - 1)
+  else s;
+
+val trim_split_lines = trim_line #> split_lines #> map trim_line;
 
 fun replicate_string (0: int) _ = ""
   | replicate_string 1 a = a