--- 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
--- 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;
--- 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;