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