# HG changeset patch
# User wenzelm
# Date 1713258046 -7200
# Node ID c729b1d589820eb1447712c43ac5330a97ef6c53
# Parent  f4d3e39152286ece6316c4ba3168a3d4224b3f54
more robust tmp_file (see also ab07d4cb7d1c and 146468e05dd4);

diff -r f4d3e3915228 -r c729b1d58982 src/Pure/ML/ml_heap.scala
--- a/src/Pure/ML/ml_heap.scala	Fri Apr 12 17:07:33 2024 +0200
+++ b/src/Pure/ML/ml_heap.scala	Tue Apr 16 11:00:46 2024 +0200
@@ -285,15 +285,12 @@
 
             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)
+              tmp.file.delete()
               for (slice <- private_data.read_slices(db, session_name)) {
                 Bytes.append(tmp, slice.uncompress(cache = cache))
               }
               val digest = write_file_digest(tmp)
-              if (db_digest.get == digest) {
-                Isabelle_System.chmod("a+r", tmp)
-                Isabelle_System.move_file(tmp, heap)
-              }
+              if (db_digest.get == digest) Isabelle_System.move_file(tmp, heap)
               else error("Incoherent content for session heap " + heap.expand)
             }
           }