# HG changeset patch # User wenzelm # Date 1598095318 -7200 # Node ID b155681b9f6a01290d5bbc64427fa6d40dadcd76 # Parent e4aecb0c729687423a6494aaeee6a198cd101db7 removed obsolete created_temp_dir: ISABELLE_TMP is always present for the running Isabelle/ML process; diff -r e4aecb0c7296 -r b155681b9f6a src/HOL/Tools/Nitpick/kodkod.ML --- a/src/HOL/Tools/Nitpick/kodkod.ML Fri Aug 21 18:59:30 2020 +0000 +++ b/src/HOL/Tools/Nitpick/kodkod.ML Sat Aug 22 13:21:58 2020 +0200 @@ -970,19 +970,12 @@ |>> rev ||> rev) handle IO.Io _ => (true, ([], [])) | OS.SysErr _ => (true, ([], [])) + (** Main Kodkod entry point **) -val created_temp_dir = Unsynchronized.ref false - -fun serial_string_and_temporary_dir_for_overlord overlord = - if overlord then - ("", getenv "ISABELLE_HOME_USER") - else - let - val dir = getenv "ISABELLE_TMP" - val _ = if !created_temp_dir then () - else (created_temp_dir := true; Isabelle_System.mkdirs (Path.explode dir)) - in (serial_string (), dir) end +fun serial_string_and_temporary_dir overlord = + if overlord then ("", getenv "ISABELLE_HOME_USER") + else (serial_string (), getenv "ISABELLE_TMP") (* The fudge term below is to account for Kodkodi's slow start-up time, which is partly due to the JVM and partly due to the ML "bash" function. *) @@ -1008,8 +1001,7 @@ Normal ([], triv_js, "") else let - val (serial_str, temp_dir) = - serial_string_and_temporary_dir_for_overlord overlord + val (serial_str, temp_dir) = serial_string_and_temporary_dir overlord fun path_for suf = Path.explode (temp_dir ^ "/kodkodi" ^ serial_str ^ "." ^ suf) val in_path = path_for "kki"