# HG changeset patch
# User wenzelm
# Date 1456350019 -3600
# Node ID 15a2533f1f0ad5ef63532d1996028bb4f0407353
# Parent  833af0d6d4695620e74f689457249cd479a07223
more informative Process_Result;
tuned;

diff -r 833af0d6d469 -r 15a2533f1f0a src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Wed Feb 24 22:11:28 2016 +0100
+++ b/src/Pure/System/isabelle_system.scala	Wed Feb 24 22:40:19 2016 +0100
@@ -337,7 +337,7 @@
         catch { case Exn.Interrupt() => proc.terminate; Exn.Interrupt.return_code }
       if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
 
-      Process_Result(stdout.join, stderr.join, rc)
+      Process_Result(stdout.join, stderr.join, rc, None)
     }
   }
 
diff -r 833af0d6d469 -r 15a2533f1f0a src/Pure/System/process_result.scala
--- a/src/Pure/System/process_result.scala	Wed Feb 24 22:11:28 2016 +0100
+++ b/src/Pure/System/process_result.scala	Wed Feb 24 22:40:19 2016 +0100
@@ -6,7 +6,8 @@
 
 package isabelle
 
-final case class Process_Result(out_lines: List[String], err_lines: List[String], rc: Int)
+final case class Process_Result(
+  out_lines: List[String], err_lines: List[String], rc: Int, timeout: Option[Time])
 {
   def out: String = cat_lines(out_lines)
   def err: String = cat_lines(err_lines)
@@ -14,6 +15,8 @@
   def error(s: String, err_rc: Int = 0): Process_Result =
     copy(err_lines = err_lines ::: List(s), rc = rc max err_rc)
 
+  def set_timeout(t: Time): Process_Result = copy(timeout = Some(t))
+
   def ok: Boolean = rc == 0
   def interrupted: Boolean = rc == Exn.Interrupt.return_code
 
@@ -26,6 +29,6 @@
   {
     Output.warning(Library.trim_line(err))
     Output.writeln(Library.trim_line(out))
-    Process_Result(Nil, Nil, rc)
+    copy(out_lines = Nil, err_lines = Nil)
   }
 }
diff -r 833af0d6d469 -r 15a2533f1f0a src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Feb 24 22:11:28 2016 +0100
+++ b/src/Pure/Tools/build.scala	Wed Feb 24 22:40:19 2016 +0100
@@ -619,12 +619,13 @@
     def terminate: Unit = result.cancel
     def is_finished: Boolean = result.is_finished
 
-    @volatile private var was_timeout = false
+    @volatile private var was_timeout: Option[Time] = None
     private val timeout_request: Option[Event_Timer.Request] =
     {
       val timeout = info.timeout
+      val t0 = Time.now()
       if (timeout > Time.zero)
-        Some(Event_Timer.request(Time.now() + timeout) { terminate; was_timeout = true })
+        Some(Event_Timer.request(t0 + timeout) { terminate; was_timeout = Some(Time.now() - t0) })
       else None
     }
 
@@ -639,9 +640,11 @@
       args_file.delete
       timeout_request.foreach(_.cancel)
 
-      if (res.rc == Exn.Interrupt.return_code) {
-        if (was_timeout) res.error(Output.error_text("Timeout"), 1)
-        else res.error(Output.error_text("Interrupt"))
+      if (res.interrupted) {
+        was_timeout match {
+          case Some(t) => res.error(Output.error_text("Timeout"), 1).set_timeout(t)
+          case None => res.error(Output.error_text("Interrupt"))
+        }
       }
       else res
     }
@@ -854,17 +857,17 @@
           case Some((name, (parent_heap, job))) =>
             //{{{ finish job
 
-            val res = job.join
-            progress.echo(res.err)
+            val process_result = job.join
+            progress.echo(process_result.err)
 
             val heap =
-              if (res.ok) {
+              if (process_result.ok) {
                 (output_dir + log(name)).file.delete
 
                 val sources = make_stamp(name)
                 val heap = heap_stamp(job.output_path)
                 File.write_gzip(output_dir + log_gz(name),
-                  Library.terminate_lines(sources :: parent_heap :: heap :: res.out_lines))
+                  Library.terminate_lines(sources :: parent_heap :: heap :: process_result.out_lines))
 
                 heap
               }
@@ -872,11 +875,11 @@
                 (output_dir + Path.basic(name)).file.delete
                 (output_dir + log_gz(name)).file.delete
 
-                File.write(output_dir + log(name), Library.terminate_lines(res.out_lines))
+                File.write(output_dir + log(name), Library.terminate_lines(process_result.out_lines))
                 progress.echo(name + " FAILED")
-                if (res.rc != Exn.Interrupt.return_code) {
+                if (!process_result.interrupted) {
                   progress.echo("(see also " + (output_dir + log(name)).file.toString + ")")
-                  val lines = res.out_lines.filterNot(_.startsWith("\f"))
+                  val lines = process_result.out_lines.filterNot(_.startsWith("\f"))
                   val tail = lines.drop(lines.length - 20 max 0)
                   progress.echo("\n" + cat_lines(tail))
                 }
@@ -884,7 +887,7 @@
                 no_heap
               }
             loop(pending - name, running - name,
-              results + (name -> Result(false, heap, res.rc)))
+              results + (name -> Result(false, heap, process_result.rc)))
             //}}}
           case None if running.size < (max_jobs max 1) =>
             //{{{ check/start next job