create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);
authorwenzelm
Sat, 12 Mar 2016 21:23:58 +0100
changeset 62601 a937889f0086
parent 62600 614aefb0e6cc
child 62602 96e679f042ec
create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);
src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
src/Pure/Tools/ml_process.scala
--- 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
--- 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)
   }