# HG changeset patch
# User wenzelm
# Date 1614008741 -3600
# Node ID 7dbae202ff848a52c64509fb444877851688478b
# Parent  0110e2e2964ce30713dbc8b177247dc8fa25d70e
clarified signature: Isabelle_System.bash_process is strict and thus cannot check for interrupt_return_code;

diff -r 0110e2e2964c -r 7dbae202ff84 src/Pure/General/exn.ML
--- 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);
diff -r 0110e2e2964c -r 7dbae202ff84 src/Pure/System/process_result.ML
--- 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;