clarified signature: Isabelle_System.bash_process is strict and thus cannot check for interrupt_return_code;
--- a/src/Pure/General/exn.ML Mon Feb 22 15:24:04 2021 +0100
+++ b/src/Pure/General/exn.ML Mon Feb 22 16:45:41 2021 +0100
@@ -30,7 +30,6 @@
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
@@ -105,10 +104,8 @@
(* POSIX return code *)
-val interrupt_return_code : int = 130;
-
fun return_code exn rc =
- if is_interrupt exn then interrupt_return_code else rc;
+ if is_interrupt exn then 130 else rc;
fun capture_exit rc f x =
f x handle exn => exit (return_code exn rc);
--- a/src/Pure/System/process_result.ML Mon Feb 22 15:24:04 2021 +0100
+++ b/src/Pure/System/process_result.ML Mon Feb 22 16:45:41 2021 +0100
@@ -19,8 +19,6 @@
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;
@@ -47,14 +45,8 @@
val err = trim_line o 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);
+fun check result = if ok result then result else error (err result);
end;