removed obsolete created_temp_dir: ISABELLE_TMP is always present for the running Isabelle/ML process;
authorwenzelm
Sat, 22 Aug 2020 13:21:58 +0200
changeset 72188 b155681b9f6a
parent 72187 e4aecb0c7296
child 72189 7a213affdc10
removed obsolete created_temp_dir: ISABELLE_TMP is always present for the running Isabelle/ML process;
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"