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