--- a/src/HOL/Tools/Nunchaku/nunchaku_tool.ML Mon Feb 22 13:29:55 2021 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_tool.ML Mon Feb 22 14:48:03 2021 +0100
@@ -103,7 +103,10 @@
[bash_cmd, "This file was generated by Isabelle (most likely Nunchaku)", timestamp ()];
val prob_str = cat_lines (map (prefix "# ") comments) ^ "\n\n" ^ str_of_nun_problem problem;
val _ = File.write prob_path prob_str;
- val {out, err, rc, ...} = Isabelle_System.bash_process bash_cmd;
+ val res = Isabelle_System.bash_process bash_cmd;
+ val rc = Process_Result.rc res;
+ val out = Process_Result.out res;
+ val err = Process_Result.err res;
val backend =
(case map_filter (try (unprefix "{backend:")) (split_lines out) of
--- a/src/Pure/General/exn.ML Mon Feb 22 13:29:55 2021 +0100
+++ b/src/Pure/General/exn.ML Mon Feb 22 14:48:03 2021 +0100
@@ -30,6 +30,7 @@
val interrupt_exn: 'a result
val is_interrupt_exn: 'a result -> bool
val interruptible_capture: ('a -> 'b) -> 'a -> 'b result
+ val interrupt_return_code: int
val return_code: exn -> int -> int
val capture_exit: int -> ('a -> 'b) -> 'a -> 'b
exception EXCEPTIONS of exn list
@@ -104,8 +105,10 @@
(* POSIX return code *)
+val interrupt_return_code : int = 130;
+
fun return_code exn rc =
- if is_interrupt exn then (130: int) else rc;
+ if is_interrupt exn then interrupt_return_code else rc;
fun capture_exit rc f x =
f x handle exn => exit (return_code exn rc);
--- a/src/Pure/ROOT.ML Mon Feb 22 13:29:55 2021 +0100
+++ b/src/Pure/ROOT.ML Mon Feb 22 14:48:03 2021 +0100
@@ -294,6 +294,7 @@
(*Isabelle system*)
ML_file "PIDE/protocol_command.ML";
ML_file "System/scala.ML";
+ML_file "System/process_result.ML";
ML_file "System/isabelle_system.ML";
--- a/src/Pure/System/isabelle_system.ML Mon Feb 22 13:29:55 2021 +0100
+++ b/src/Pure/System/isabelle_system.ML Mon Feb 22 14:48:03 2021 +0100
@@ -6,14 +6,7 @@
signature ISABELLE_SYSTEM =
sig
- type process_result =
- {rc: int,
- out_lines: string list,
- err_lines: string list,
- out: string,
- err: string,
- timing: Timing.timing}
- val bash_process: string -> process_result
+ val bash_process: string -> Process_Result.T
val bash_output_check: string -> string
val bash_output: string -> string * int
val bash: string -> int
@@ -36,15 +29,7 @@
(* bash *)
-type process_result =
- {rc: int,
- out_lines: string list,
- err_lines: string list,
- out: string,
- err: string,
- timing: Timing.timing};
-
-fun bash_process script : process_result =
+fun bash_process script =
Scala.function_thread "bash_process"
("export ISABELLE_TMP=" ^ Bash.string (getenv "ISABELLE_TMP") ^ "\n" ^ script)
|> space_explode "\000"
@@ -54,28 +39,27 @@
let
val rc = Value.parse_int a;
val (elapsed, cpu) = apply2 (Time.fromMilliseconds o Value.parse_int) (b, c);
- val ((out, err), (out_lines, err_lines)) =
- chop (Value.parse_int d) lines |> `(apply2 cat_lines);
+ val (out_lines, err_lines) = chop (Value.parse_int d) lines;
in
- {rc = rc,
- out_lines = out_lines,
- err_lines = err_lines,
- out = out,
- err = err,
- timing = {elapsed = elapsed, cpu = cpu, gc = Time.zeroTime}}
+ Process_Result.make
+ {rc = rc,
+ out_lines = out_lines,
+ err_lines = err_lines,
+ timing = {elapsed = elapsed, cpu = cpu, gc = Time.zeroTime}}
end
| _ => raise Fail "Malformed Isabelle/Scala result");
fun bash_output_check s =
- (case bash_process s of
- {rc = 0, out, ...} => trim_line out
- | {err, ...} => error (trim_line err));
+ let val res = bash_process s in
+ if Process_Result.ok res then trim_line (Process_Result.out res)
+ else error (trim_line (Process_Result.err res))
+ end;
fun bash_output s =
let
- val {out, err, rc, ...} = bash_process s;
- val _ = warning (trim_line err);
- in (out, rc) end;
+ val res = bash_process s;
+ val _ = warning (trim_line (Process_Result.err res));
+ in (Process_Result.out res, Process_Result.rc res) end;
fun bash s =
let
@@ -164,9 +148,12 @@
fun download url =
with_tmp_file "download" "" (fn path =>
- ("curl --fail --silent --location " ^ Bash.string url ^ " > " ^ File.bash_path path)
- |> bash_process
- |> (fn {rc = 0, ...} => File.read path
- | {err, ...} => cat_error ("Failed to download " ^ quote url) err));
+ let
+ val s = "curl --fail --silent --location " ^ Bash.string url ^ " > " ^ File.bash_path path;
+ val res = bash_process s;
+ in
+ if Process_Result.ok res then File.read path
+ else cat_error ("Failed to download " ^ quote url) (Process_Result.err res)
+ end);
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/process_result.ML Mon Feb 22 14:48:03 2021 +0100
@@ -0,0 +1,61 @@
+(* Title: Pure/System/process_result.scala
+ Author: Makarius
+
+Result of system process.
+*)
+
+signature PROCESS_RESULT =
+sig
+ type T
+ val make:
+ {rc: int,
+ out_lines: string list,
+ err_lines: string list,
+ timing: Timing.timing} -> T
+ val rc: T -> int
+ val out_lines: T -> string list
+ val err_lines: T -> string list
+ val timing: T -> Timing.timing
+ val out: T -> string
+ val err: T -> string
+ val ok: T -> bool
+ val interrupted: T -> bool
+ val check_rc: (int -> bool) -> T -> T
+ val check: T -> T
+end;
+
+structure Process_Result: PROCESS_RESULT =
+struct
+
+abstype T =
+ Process_Result of
+ {rc: int,
+ out_lines: string list,
+ err_lines: string list,
+ timing: Timing.timing}
+with
+
+val make = Process_Result;
+fun rep (Process_Result args) = args;
+
+val rc = #rc o rep;
+val out_lines = #out_lines o rep;
+val err_lines = #err_lines o rep;
+val timing = #timing o rep;
+
+val out = cat_lines o out_lines;
+val err = cat_lines o err_lines;
+
+fun ok result = rc result = 0;
+fun interrupted result = rc result = Exn.interrupt_return_code;
+
+fun check_rc pred result =
+ if pred (rc result) then result
+ else if interrupted result then raise Exn.Interrupt
+ else error (err result);
+
+val check = check_rc (fn rc => rc = 0);
+
+end;
+
+end;