--- 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")
}
}
}
--- 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