clarified signature: always trim_line of Process_Result.out/err, uniformly in ML and Scala;
--- 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 *)
--- 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 =
--- 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))
}
--- 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;
--- 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;
--- 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))
--- 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)