# HG changeset patch
# User wenzelm
# Date 1457814238 -3600
# Node ID a937889f008649799bc0fdb67165235b8044364e
# Parent  614aefb0e6cc5afabdf3d05ef34b1187d734f301
create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);

diff -r 614aefb0e6cc -r a937889f0086 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Sat Mar 12 21:03:45 2016 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Sat Mar 12 21:23:58 2016 +0100
@@ -315,7 +315,6 @@
     val ctxt = Proof.context_of state
 
     val override_params = override_params |> map (normalize_raw_param ctxt)
-    val _ = Isabelle_System.mkdir (Path.explode (getenv "ISABELLE_TMP"))
   in
     if subcommand = runN then
       let val i = the_default 1 opt_i in
diff -r 614aefb0e6cc -r a937889f0086 src/Pure/Tools/ml_process.scala
--- a/src/Pure/Tools/ml_process.scala	Sat Mar 12 21:03:45 2016 +0100
+++ b/src/Pure/Tools/ml_process.scala	Sat Mar 12 21:23:58 2016 +0100
@@ -87,6 +87,10 @@
               ML_Syntax.print_string_raw(ch.server_name) + ")")
         }
 
+    // ISABELLE_TMP
+    val isabelle_tmp = Isabelle_System.tmp_dir("process")
+    val env_tmp = Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp))
+
     // bash
     val bash_args =
       Word.explode(Isabelle_System.getenv("ML_OPTIONS")) :::
@@ -95,21 +99,15 @@
 
     Bash.process(
       """
-        [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
-
-        export ISABELLE_TMP="$ISABELLE_TMP_PREFIX$$"
-        mkdir -p "$ISABELLE_TMP"
-        chmod $(umask -S) "$ISABELLE_TMP"
-
         librarypath "$ML_HOME"
         "$ML_HOME/poly" -q """ + File.bash_args(bash_args) + """
         RC="$?"
 
-        rm -f "$ISABELLE_PROCESS_OPTIONS"
+        [ -e "$ISABELLE_PROCESS_OPTIONS" ] && rm -f "$ISABELLE_PROCESS_OPTIONS"
         rmdir "$ISABELLE_TMP"
 
         exit "$RC"
-      """, cwd = cwd, env = env ++ env_options, redirect = redirect)
+      """, cwd = cwd, env = env ++ env_options ++ env_tmp, redirect = redirect)
   }