more robust tmp_file (see also ab07d4cb7d1c and 146468e05dd4);
authorwenzelm
Tue, 16 Apr 2024 11:00:46 +0200
changeset 80112 c729b1d58982
parent 80111 f4d3e3915228
child 80113 4b95a1d8b2c9
more robust tmp_file (see also ab07d4cb7d1c and 146468e05dd4);
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)
             }
           }