bash process with builtin timing;

--- a/Admin/components/components.sha1	Wed Mar 09 14:24:16 2016 +0100
+++ b/Admin/components/components.sha1	Wed Mar 09 14:54:51 2016 +0100
@@ -1,5 +1,6 @@
 fbe83b522cb37748ac1b3c943ad71704fdde2f82  bash_process-1.1.1.tar.gz
 bb9ef498cd594b4289221b96146d529c899da209  bash_process-1.1.tar.gz
+9e21f447bfa0431ae5097301d553dd6df3c58218  bash_process-1.2.tar.gz
 70105fd6fbfd1a868383fc510772b95234325d31  csdp-6.x.tar.gz
 2f6417b8e96a0e4e8354fe0f1a253c18fb55d9a7  cvc3-2.4.1.tar.gz
 a5e02b5e990da4275dc5d4480c3b72fc73160c28  cvc4-1.5pre-1.tar.gz

--- a/Admin/components/main	Wed Mar 09 14:24:16 2016 +0100
+++ b/Admin/components/main	Wed Mar 09 14:54:51 2016 +0100
@@ -1,5 +1,5 @@
 #main components for everyday use, without big impact on overall build time
-bash_process-1.1.1
+bash_process-1.2
 csdp-6.x
 cvc4-1.5pre-3
 e-1.8

--- a/src/Pure/Concurrent/bash.ML	Wed Mar 09 14:24:16 2016 +0100
+++ b/src/Pure/Concurrent/bash.ML	Wed Mar 09 14:54:51 2016 +0100
@@ -38,7 +38,7 @@
             val _ = getenv_strict "ISABELLE_BASH_PROCESS";
             val status =
               OS.Process.system
-                ("exec \"$ISABELLE_BASH_PROCESS\" " ^ File.bash_path pid_path ^
+                ("exec \"$ISABELLE_BASH_PROCESS\" " ^ File.bash_path pid_path ^ " \"\"" ^
                   " bash " ^ File.bash_path script_path ^
                   " > " ^ File.bash_path out_path ^
                   " 2> " ^ File.bash_path err_path);

--- a/src/Pure/Concurrent/bash.scala	Wed Mar 09 14:24:16 2016 +0100
+++ b/src/Pure/Concurrent/bash.scala	Wed Mar 09 14:54:51 2016 +0100
@@ -34,13 +34,16 @@
       script: String, cwd: JFile, env: Map[String, String], redirect: Boolean)
     extends Prover.System_Process
   {
-    val script_file = Isabelle_System.tmp_file("bash_script")
+    private val timing_file = Isabelle_System.tmp_file("bash_script")
+    private val timing = Synchronized[Option[Timing]](None)
+
+    private val script_file = Isabelle_System.tmp_file("bash_script")
     File.write(script_file, script)
 
     private val proc =
       Isabelle_System.process(cwd, Isabelle_System.settings(env), redirect,
         File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), "-",
-          "bash", File.standard_path(script_file))
+          File.standard_path(timing_file), "bash", File.standard_path(script_file))
 
 
     // channels
@@ -105,6 +108,19 @@
 
       script_file.delete
 
+      timing.change {
+        case None =>
+          val t =
+            Word.explode(File.read(timing_file)) match {
+              case List(Properties.Value.Long(elapsed), Properties.Value.Long(cpu)) =>
+                Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero)
+              case _ => Timing.zero
+            }
+          timing_file.delete
+          Some(t)
+        case some => some
+      }
+
       rc
     }
 
@@ -130,7 +146,7 @@
         catch { case Exn.Interrupt() => terminate; Exn.Interrupt.return_code }
       if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
 
-      Process_Result(rc, out_lines.join, err_lines.join)
+      Process_Result(rc, out_lines.join, err_lines.join, false, timing.value.get)
     }
   }
 }

--- a/src/Pure/Concurrent/bash_windows.ML	Wed Mar 09 14:24:16 2016 +0100
+++ b/src/Pure/Concurrent/bash_windows.ML	Wed Mar 09 14:54:51 2016 +0100
@@ -43,7 +43,7 @@
             val rc =
               Windows.simpleExecute ("",
                 quote (ML_System.platform_path bash_process) ^ " " ^
-                quote (File.platform_path pid_path) ^ " bash -c " ^ quote bash_script)
+                quote (File.platform_path pid_path) ^  " \"\" bash -c " ^ quote bash_script)
               |> Windows.fromStatus |> SysWord.toInt;
             val res = if rc = 130 orelse rc = 512 then Signal else Result rc;
           in Synchronized.change result (K res) end

--- a/src/Pure/System/process_result.scala	Wed Mar 09 14:24:16 2016 +0100
+++ b/src/Pure/System/process_result.scala	Wed Mar 09 14:54:51 2016 +0100
@@ -10,13 +10,14 @@
   rc: Int,
   out_lines: List[String] = Nil,
   err_lines: List[String] = Nil,
-  timeout: Option[Time] = None)
+  timeout: Boolean = false,
+  timing: Timing = Timing.zero)
 {
   def out: String = cat_lines(out_lines)
   def err: String = cat_lines(err_lines)
   def error(s: String): Process_Result = copy(err_lines = err_lines ::: List(s))
 
-  def set_timeout(t: Time): Process_Result = copy(rc = 1, timeout = Some(t))
+  def was_timeout: Process_Result = copy(rc = 1, timeout = true)
 
   def ok: Boolean = rc == 0
   def interrupted: Boolean = rc == Exn.Interrupt.return_code

--- a/src/Pure/Tools/build.scala	Wed Mar 09 14:24:16 2016 +0100
+++ b/src/Pure/Tools/build.scala	Wed Mar 09 14:54:51 2016 +0100
@@ -624,13 +624,11 @@
     def terminate: Unit = result.cancel
     def is_finished: Boolean = result.is_finished
 
-    @volatile private var was_timeout: Option[Time] = None
+    @volatile private var was_timeout = false
     private val timeout_request: Option[Event_Timer.Request] =
     {
-      val timeout = info.timeout
-      val t0 = Time.now()
-      if (timeout > Time.zero)
-        Some(Event_Timer.request(t0 + timeout) { terminate; was_timeout = Some(Time.now() - t0) })
+      if (info.timeout > Time.zero)
+        Some(Event_Timer.request(Time.now() + info.timeout) { terminate; was_timeout = true })
       else None
     }
 
@@ -646,10 +644,8 @@
       timeout_request.foreach(_.cancel)
 
       if (res.interrupted) {
-        was_timeout match {
-          case Some(t) => res.error(Output.error_text("Timeout")).set_timeout(t)
-          case None => res.error(Output.error_text("Interrupt"))
-        }
+        if (was_timeout) res.error(Output.error_text("Timeout")).was_timeout
+        else res.error(Output.error_text("Interrupt"))
       }
       else res
     }