# HG changeset patch
# User wenzelm
# Date 1614009273 -3600
# Node ID 37aff2142295746ac7febdea2bf6c65d953e57d2
# Parent  7dbae202ff848a52c64509fb444877851688478b
clarified signature;

diff -r 7dbae202ff84 -r 37aff2142295 src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Mon Feb 22 16:45:41 2021 +0100
+++ b/src/Pure/System/isabelle_system.ML	Mon Feb 22 16:54:33 2021 +0100
@@ -7,7 +7,6 @@
 signature ISABELLE_SYSTEM =
 sig
   val bash_process: string -> Process_Result.T
-  val bash_output_check: string -> string
   val bash_output: string -> string * int
   val bash: string -> int
   val bash_functions: unit -> string list
@@ -49,12 +48,6 @@
          end
       | _ => raise Fail "Malformed Isabelle/Scala result");
 
-fun bash_output_check s =
-  let val res = bash_process s in
-    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;
@@ -71,8 +64,10 @@
 (* bash functions *)
 
 fun bash_functions () =
-  bash_output_check "declare -Fx"
-  |> split_lines |> map_filter (space_explode " " #> try List.last);
+  bash_process "declare -Fx"
+  |> Process_Result.check
+  |> Process_Result.out_lines
+  |> map_filter (space_explode " " #> try List.last);
 
 fun check_bash_function ctxt arg =
   Completion.check_entity Markup.bash_functionN
diff -r 7dbae202ff84 -r 37aff2142295 src/Pure/Tools/generated_files.ML
--- a/src/Pure/Tools/generated_files.ML	Mon Feb 22 16:45:41 2021 +0100
+++ b/src/Pure/Tools/generated_files.ML	Mon Feb 22 16:54:33 2021 +0100
@@ -332,7 +332,9 @@
 (* execute compiler -- auxiliary *)
 
 fun execute dir title compile =
-  Isabelle_System.bash_output_check ("cd " ^ File.bash_path dir ^ " && " ^ compile)
+  Isabelle_System.bash_process ("cd " ^ File.bash_path dir ^ " && " ^ compile)
+  |> Process_Result.check
+  |> Process_Result.out
     handle ERROR msg =>
       let val (s, pos) = Input.source_content title
       in error (s ^ " failed" ^ Position.here pos ^ ":\n" ^ msg) end;
diff -r 7dbae202ff84 -r 37aff2142295 src/Pure/Tools/ghc.ML
--- a/src/Pure/Tools/ghc.ML	Mon Feb 22 16:45:41 2021 +0100
+++ b/src/Pure/Tools/ghc.ML	Mon Feb 22 16:54:33 2021 +0100
@@ -84,9 +84,10 @@
     val template_path = dir + (Path.basic name |> Path.ext "hsfiles");
     val _ = File.write template_path (project_template {depends = depends, modules = modules});
     val _ =
-      Isabelle_System.bash_output_check
+      Isabelle_System.bash_process
         ("cd " ^ File.bash_path dir ^ "; isabelle ghc_stack new " ^ Bash.string name ^
-          " --bare " ^ File.bash_platform_path template_path);
+          " --bare " ^ File.bash_platform_path template_path)
+      |> Process_Result.check;
   in () end;
 
 end;