# HG changeset patch
# User wenzelm
# Date 1457549537 -3600
# Node ID ec382bc689e5990f2b353fe9c49c388bf8b0ede8
# Parent  27f90319a499981eaa649ced73e7de58b999b390
more robust cleanup;
more defensive timing value;

diff -r 27f90319a499 -r ec382bc689e5 src/Pure/Concurrent/bash.scala
--- a/src/Pure/Concurrent/bash.scala	Wed Mar 09 19:30:09 2016 +0100
+++ b/src/Pure/Concurrent/bash.scala	Wed Mar 09 19:52:17 2016 +0100
@@ -88,7 +88,12 @@
       running
     }
 
-    def terminate() { multi_kill("INT") && multi_kill("TERM") && kill("KILL"); proc.destroy }
+    def terminate()
+    {
+      multi_kill("INT") && multi_kill("TERM") && kill("KILL")
+      proc.destroy
+      cleanup()
+    }
 
 
     // JVM shutdown hook
@@ -99,12 +104,10 @@
     catch { case _: IllegalStateException => }
 
 
-    /* join */
+    // cleanup
 
-    def join: Int =
+    private def cleanup()
     {
-      val rc = proc.waitFor
-
       try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
       catch { case _: IllegalStateException => }
 
@@ -112,22 +115,33 @@
 
       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)
+          if (timing_file.isFile) {
+            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)
+          }
+          else Some(Timing.zero)
         case some => some
       }
+    }
 
+
+    // join
+
+    def join: Int =
+    {
+      val rc = proc.waitFor
+      cleanup()
       rc
     }
 
 
-    /* result */
+    // result
 
     def result(
       progress_stdout: String => Unit = (_: String) => (),
@@ -145,10 +159,10 @@
 
       val rc =
         try { join }
-        catch { case Exn.Interrupt() => terminate; Exn.Interrupt.return_code }
+        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, false, timing.value.get)
+      Process_Result(rc, out_lines.join, err_lines.join, false, timing.value getOrElse Timing.zero)
     }
   }
 }