# HG changeset patch
# User wenzelm
# Date 1614003844 -3600
# Node ID 0110e2e2964ce30713dbc8b177247dc8fa25d70e
# Parent  54065cbf71347bb2a6ad5d35457e2023b155e42d
clarified signature: always trim_line of Process_Result.out/err, uniformly in ML and Scala;

diff -r 54065cbf7134 -r 0110e2e2964c src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Mon Feb 22 15:20:45 2021 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Mon Feb 22 15:24:04 2021 +0100
@@ -865,7 +865,7 @@
         (l :: r :: []) => parse_term (unprefix " " r)
       | _ => raise Fail "unexpected equation in prolog output")
     fun parse_solution s = map dest_eq (space_explode ";" s)
-  in map parse_solution (Library.trim_split_lines sol) end
+  in map parse_solution (split_lines sol) end
 
 
 (* calling external interpreter and getting results *)
diff -r 54065cbf7134 -r 0110e2e2964c src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Mon Feb 22 15:20:45 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Mon Feb 22 15:24:04 2021 +0100
@@ -574,7 +574,7 @@
       (warning
          (case extract_known_atp_failure known_perl_failures output of
            SOME failure => string_of_atp_failure failure
-         | NONE => trim_line output); []))) ()
+         | NONE => output); []))) ()
   handle Timeout.TIMEOUT _ => []
 
 fun find_remote_system name [] systems =
diff -r 54065cbf7134 -r 0110e2e2964c src/Pure/Admin/components.scala
--- a/src/Pure/Admin/components.scala	Mon Feb 22 15:20:45 2021 +0100
+++ b/src/Pure/Admin/components.scala	Mon Feb 22 15:24:04 2021 +0100
@@ -279,9 +279,8 @@
                 }
                 yield {
                   progress.echo("Digesting remote " + entry.name)
-                  Library.trim_line(
-                    ssh.execute("cd " + ssh.bash_path(components_dir) +
-                      "; sha1sum " + Bash.string(entry.name)).check.out)
+                  ssh.execute("cd " + ssh.bash_path(components_dir) +
+                    "; sha1sum " + Bash.string(entry.name)).check.out
                 }
               write_components_sha1(read_components_sha1(lines))
             }
diff -r 54065cbf7134 -r 0110e2e2964c src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Mon Feb 22 15:20:45 2021 +0100
+++ b/src/Pure/System/isabelle_system.ML	Mon Feb 22 15:24:04 2021 +0100
@@ -51,20 +51,20 @@
 
 fun bash_output_check s =
   let val res = bash_process s in
-    if Process_Result.ok res then trim_line (Process_Result.out res)
-    else error (trim_line (Process_Result.err res))
+    if Process_Result.ok res then Process_Result.out res
+    else error (Process_Result.err res)
   end;
 
 fun bash_output s =
   let
     val res = bash_process s;
-    val _ = warning (trim_line (Process_Result.err res));
+    val _ = warning (Process_Result.err res);
   in (Process_Result.out res, Process_Result.rc res) end;
 
 fun bash s =
   let
     val (out, rc) = bash_output s;
-    val _ = writeln (trim_line out);
+    val _ = writeln out;
   in rc end;
 
 
diff -r 54065cbf7134 -r 0110e2e2964c src/Pure/System/process_result.ML
--- a/src/Pure/System/process_result.ML	Mon Feb 22 15:20:45 2021 +0100
+++ b/src/Pure/System/process_result.ML	Mon Feb 22 15:24:04 2021 +0100
@@ -43,8 +43,8 @@
 val err_lines = #err_lines o rep;
 val timing = #timing o rep;
 
-val out = cat_lines o out_lines;
-val err = cat_lines o err_lines;
+val out = trim_line o cat_lines o out_lines;
+val err = trim_line o cat_lines o err_lines;
 
 fun ok result = rc result = 0;
 fun interrupted result = rc result = Exn.interrupt_return_code;
diff -r 54065cbf7134 -r 0110e2e2964c src/Pure/System/process_result.scala
--- a/src/Pure/System/process_result.scala	Mon Feb 22 15:20:45 2021 +0100
+++ b/src/Pure/System/process_result.scala	Mon Feb 22 15:24:04 2021 +0100
@@ -38,8 +38,8 @@
   err_lines: List[String] = Nil,
   timing: Timing = Timing.zero)
 {
-  def out: String = cat_lines(out_lines)
-  def err: String = cat_lines(err_lines)
+  def out: String = Library.trim_line(cat_lines(out_lines))
+  def err: String = Library.trim_line(cat_lines(err_lines))
 
   def output(outs: List[String]): Process_Result =
     copy(out_lines = out_lines ::: outs.flatMap(split_lines))
diff -r 54065cbf7134 -r 0110e2e2964c src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Mon Feb 22 15:20:45 2021 +0100
+++ b/src/Pure/Thy/presentation.scala	Mon Feb 22 15:24:04 2021 +0100
@@ -680,7 +680,7 @@
             if (!result.ok) {
               val message =
                 Exn.cat_message(
-                  Library.trim_line(result.err),
+                  result.err,
                   cat_lines(Latex.latex_errors(doc_dir, root) ::: Bibtex.bibtex_errors(doc_dir, root)),
                   "Failed to build document " + quote(doc.name))
               throw new Build_Error(log_lines, message)