# HG changeset patch
# User wenzelm
# Date 1554380989 -7200
# Node ID 5b66e6672ccf92f88fe3a58d79e772c508867dc6
# Parent  c1226e4c273e285d24f86a900d5fdf9b523482c8
tuned signature: more operations;

diff -r c1226e4c273e -r 5b66e6672ccf src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Wed Apr 03 23:35:13 2019 +0200
+++ b/src/Pure/System/isabelle_system.ML	Thu Apr 04 14:29:49 2019 +0200
@@ -15,6 +15,7 @@
   val create_tmp_path: string -> string -> Path.T
   val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a
   val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
+  val bash_output_check: string -> string
   val bash_output: string -> string * int
   val bash: string -> int
 end;
@@ -24,6 +25,11 @@
 
 (* bash *)
 
+fun bash_output_check s =
+  (case Bash.process s of
+    {rc = 0, out, ...} => (trim_line out)
+  | {err, ...} => error (trim_line err));
+
 fun bash_output s =
   let
     val {out, err, rc, ...} = Bash.process s;