clarified signature, following Isabelle/Scala;
authorwenzelm
Mon, 22 Feb 2021 17:17:30 +0100
changeset 73281 22417b631453
parent 73280 a96944cbaf7d
child 73282 dcadb3243cfa
clarified signature, following Isabelle/Scala;
src/Pure/System/isabelle_system.ML
src/Pure/System/process_result.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 *)
 
--- 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;