# HG changeset patch
# User wenzelm
# Date 1614010650 -3600
# Node ID 22417b6314539a67b3c06606b9093ac19378a07a
# Parent  a96944cbaf7d4247651245da7167d2b7e45088b6
clarified signature, following Isabelle/Scala;

diff -r a96944cbaf7d -r 22417b631453 src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Mon Feb 22 16:58:56 2021 +0100
+++ b/src/Pure/System/isabelle_system.ML	Mon Feb 22 17:17:30 2021 +0100
@@ -48,18 +48,14 @@
          end
       | _ => raise Fail "Malformed Isabelle/Scala result");
 
+val bash = bash_process #> Process_Result.print #> Process_Result.rc;
+
 fun bash_output s =
   let
     val res = bash_process s;
     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 out;
-  in rc end;
-
 
 (* bash functions *)
 
diff -r a96944cbaf7d -r 22417b631453 src/Pure/System/process_result.ML
--- a/src/Pure/System/process_result.ML	Mon Feb 22 16:58:56 2021 +0100
+++ b/src/Pure/System/process_result.ML	Mon Feb 22 17:17:30 2021 +0100
@@ -20,6 +20,7 @@
   val err: T -> string
   val ok: T -> bool
   val check: T -> T
+  val print: T -> T
 end;
 
 structure Process_Result: PROCESS_RESULT =
@@ -50,4 +51,9 @@
 
 fun check result = if ok result then result else error (err result);
 
+fun print result =
+ (warning (err result);
+  writeln (out result);
+  make {rc = rc result, out_lines = [], err_lines = [], timing = timing result});
+
 end;