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