# HG changeset patch
# User wenzelm
# Date 1457815591 -3600
# Node ID 96e679f042eca8bf99b74b2eacd9467afa9cabdc
# Parent  a937889f008649799bc0fdb67165235b8044364e
more thorough cleanup -- in Scala;

diff -r a937889f0086 -r 96e679f042ec src/Pure/System/bash.scala
--- 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
     }
 
diff -r a937889f0086 -r 96e679f042ec src/Pure/System/isabelle_system.scala
--- 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)
   }
 
 
diff -r a937889f0086 -r 96e679f042ec src/Pure/Tools/ml_process.scala
--- 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)
+        })
   }