# HG changeset patch
# User wenzelm
# Date 1691690303 -7200
# Node ID 146468e05dd435c0ef703c48fccc5af3f966bbb0
# Parent  ab07d4cb7d1c0ee6ae1b601b023b68cc322454e6
more robust: atomic file-system result via tmp file;

diff -r ab07d4cb7d1c -r 146468e05dd4 src/Pure/ML/ml_heap.scala
--- a/src/Pure/ML/ml_heap.scala	Thu Aug 10 19:51:43 2023 +0200
+++ b/src/Pure/ML/ml_heap.scala	Thu Aug 10 19:58:23 2023 +0200
@@ -193,13 +193,19 @@
           val file_digest = read_file_digest(heap)
 
           if (db_digest.isDefined && db_digest != file_digest) {
-            Isabelle_System.make_directory(heap.expand.dir)
-            Bytes.write(heap, Bytes.empty)
+            val base_dir = Isabelle_System.make_directory(heap.expand.dir)
+            Isabelle_System.with_tmp_file(session_name + "_", base_dir = base_dir.file) { tmp =>
+              Bytes.write(tmp, Bytes.empty)
               for (slice <- private_data.read_entry(db, session_name)) {
-                Bytes.append(heap, slice.uncompress(cache = cache))
+                Bytes.append(tmp, slice.uncompress(cache = cache))
               }
-            val digest = write_file_digest(heap)
-            if (db_digest.get != digest) error("Incoherent content for file " + heap)
+              val digest = write_file_digest(tmp)
+              if (db_digest.get == digest) {
+                Isabelle_System.chmod("a+r", tmp)
+                Isabelle_System.move_file(tmp, heap)
+              }
+              else error("Incoherent content for session heap " + quote(session_name))
+            }
           }
         }
     }