# HG changeset patch
# User wenzelm
# Date 1613993405 -3600
# Node ID 17c28251fff00434c471b12ffbccadfc180c25e6
# Parent  f5a77ee9106cd14a0c5992aa10bf7ab50c16cbbf
clarified signature: process_result timing from Isabelle/Scala;

diff -r f5a77ee9106c -r 17c28251fff0 src/Pure/System/bash.scala
--- a/src/Pure/System/bash.scala	Sun Feb 21 13:33:05 2021 +0100
+++ b/src/Pure/System/bash.scala	Mon Feb 22 12:30:05 2021 +0100
@@ -223,8 +223,11 @@
         case _ if is_interrupt => ""
         case Exn.Exn(exn) => Exn.message(exn)
         case Exn.Res(res) =>
-          (res.rc.toString :: res.out_lines.length.toString ::
-            res.out_lines ::: res.err_lines).mkString("\u0000")
+         (res.rc.toString ::
+          res.timing.elapsed.ms.toString ::
+          res.timing.cpu.ms.toString ::
+          res.out_lines.length.toString ::
+          res.out_lines ::: res.err_lines).mkString("\u0000")
       }
     }
   }
diff -r f5a77ee9106c -r 17c28251fff0 src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Sun Feb 21 13:33:05 2021 +0100
+++ b/src/Pure/System/isabelle_system.ML	Mon Feb 22 12:30:05 2021 +0100
@@ -7,7 +7,12 @@
 signature ISABELLE_SYSTEM =
 sig
   type process_result =
-    {rc: int, out_lines: string list, err_lines: string list, out: string, err: string}
+   {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_output_check: string -> string
   val bash_output: string -> string * int
@@ -32,7 +37,12 @@
 (* bash *)
 
 type process_result =
-  {rc: int, out_lines: string list, err_lines: string list, out: string, err: string};
+ {rc: int,
+  out_lines: string list,
+  err_lines: string list,
+  out: string,
+  err: string,
+  timing: Timing.timing};
 
 fun bash_process script : process_result =
   Scala.function_thread "bash_process"
@@ -40,12 +50,21 @@
   |> space_explode "\000"
   |> (fn [] => raise Exn.Interrupt
       | [err] => error err
-      | a :: b :: lines =>
+      | a :: b :: c :: d :: lines =>
           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 b) lines |> `(apply2 cat_lines);
-          in {rc = rc, out_lines = out_lines, err_lines = err_lines, out = out, err = err} end);
+              chop (Value.parse_int d) lines |> `(apply2 cat_lines);
+          in
+           {rc = rc,
+            out_lines = out_lines,
+            err_lines = err_lines,
+            out = out,
+            err = err,
+            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