--- a/src/Pure/System/bash.scala Sat Mar 12 21:23:58 2016 +0100
+++ b/src/Pure/System/bash.scala Sat Mar 12 21:46:31 2016 +0100
@@ -29,11 +29,16 @@
def process(script: String,
cwd: JFile = null,
env: Map[String, String] = Map.empty,
- redirect: Boolean = false): Process =
- new Process(script, cwd, env, redirect)
+ redirect: Boolean = false,
+ cleanup: () => Unit = () => ()): Process =
+ new Process(script, cwd, env, redirect, cleanup)
class Process private [Bash](
- script: String, cwd: JFile, env: Map[String, String], redirect: Boolean)
+ script: String,
+ cwd: JFile,
+ env: Map[String, String],
+ redirect: Boolean,
+ cleanup: () => Unit)
extends Prover.System_Process
{
private val timing_file = Isabelle_System.tmp_file("bash_script")
@@ -92,7 +97,7 @@
{
multi_kill("INT") && multi_kill("TERM") && kill("KILL")
proc.destroy
- cleanup()
+ do_cleanup()
}
@@ -106,7 +111,7 @@
// cleanup
- private def cleanup()
+ private def do_cleanup()
{
try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
catch { case _: IllegalStateException => }
@@ -128,6 +133,8 @@
else Some(Timing.zero)
case some => some
}
+
+ cleanup()
}
@@ -136,7 +143,7 @@
def join: Int =
{
val rc = proc.waitFor
- cleanup()
+ do_cleanup()
rc
}
--- a/src/Pure/System/isabelle_system.scala Sat Mar 12 21:23:58 2016 +0100
+++ b/src/Pure/System/isabelle_system.scala Sat Mar 12 21:46:31 2016 +0100
@@ -306,9 +306,11 @@
progress_stdout: String => Unit = (_: String) => (),
progress_stderr: String => Unit = (_: String) => (),
progress_limit: Option[Long] = None,
- strict: Boolean = true): Process_Result =
+ strict: Boolean = true,
+ cleanup: () => Unit = () => ()): Process_Result =
{
- Bash.process(script, cwd, env).result(progress_stdout, progress_stderr, progress_limit, strict)
+ Bash.process(script, cwd = cwd, env = env, cleanup = cleanup).
+ result(progress_stdout, progress_stderr, progress_limit, strict)
}
--- a/src/Pure/Tools/ml_process.scala Sat Mar 12 21:23:58 2016 +0100
+++ b/src/Pure/Tools/ml_process.scala Sat Mar 12 21:46:31 2016 +0100
@@ -100,14 +100,14 @@
Bash.process(
"""
librarypath "$ML_HOME"
- "$ML_HOME/poly" -q """ + File.bash_args(bash_args) + """
- RC="$?"
-
- [ -e "$ISABELLE_PROCESS_OPTIONS" ] && rm -f "$ISABELLE_PROCESS_OPTIONS"
- rmdir "$ISABELLE_TMP"
-
- exit "$RC"
- """, cwd = cwd, env = env ++ env_options ++ env_tmp, redirect = redirect)
+ exec "$ML_HOME/poly" -q """ + File.bash_args(bash_args) + """
+ """,
+ cwd = cwd, env = env ++ env_options ++ env_tmp, redirect = redirect,
+ cleanup = () =>
+ {
+ isabelle_process_options.delete
+ Isabelle_System.rm_tree(isabelle_tmp)
+ })
}