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