# HG changeset patch
# User wenzelm
# Date 1614001683 -3600
# Node ID f0db1e4c89bcfd3c41caa3a4324815dc430997e7
# Parent  10d3b49a702a6d15f63abd792a5a4669b323289f
clarified signature, following Isabelle/Scala;

diff -r 10d3b49a702a -r f0db1e4c89bc src/HOL/Tools/Nunchaku/nunchaku_tool.ML
--- 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
diff -r 10d3b49a702a -r f0db1e4c89bc src/Pure/General/exn.ML
--- 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);
diff -r 10d3b49a702a -r f0db1e4c89bc src/Pure/ROOT.ML
--- 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";
 
 
diff -r 10d3b49a702a -r f0db1e4c89bc src/Pure/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;
diff -r 10d3b49a702a -r f0db1e4c89bc src/Pure/System/process_result.ML
--- /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;