# HG changeset patch
# User wenzelm
# Date 1699788844 -3600
# Node ID c125f75a51440a1f524090c0ddeccfc871954323
# Parent  932b2a7139e2490a92a540454981fed16e57cbae
more robust: prefer strict operations;

diff -r 932b2a7139e2 -r c125f75a5144 src/Pure/General/mailman.scala
--- a/src/Pure/General/mailman.scala	Sun Nov 12 12:33:22 2023 +0100
+++ b/src/Pure/General/mailman.scala	Sun Nov 12 12:34:04 2023 +0100
@@ -376,15 +376,14 @@
       try {
         val length = connection.getContentLengthLong
         val timestamp = connection.getLastModified
-        val file = path.file
-        if (file.isFile && file.length == length && file.lastModified == timestamp) None
+        if (path.is_file && File.size(path) == length && path.file.lastModified == timestamp) None
         else {
           Isabelle_System.make_directory(path.dir)
           progress.echo("Getting " + url)
           val bytes =
             using(connection.getInputStream)(Bytes.read_stream(_, hint = length.toInt max 1024))
-          Bytes.write(file, bytes)
-          file.setLastModified(timestamp)
+          Bytes.write(path, bytes)
+          path.file.setLastModified(timestamp)
           Some(path)
         }
       }
diff -r 932b2a7139e2 -r c125f75a5144 src/Pure/ML/ml_heap.scala
--- a/src/Pure/ML/ml_heap.scala	Sun Nov 12 12:33:22 2023 +0100
+++ b/src/Pure/ML/ml_heap.scala	Sun Nov 12 12:34:04 2023 +0100
@@ -21,7 +21,7 @@
     if (heap.is_file) {
       val l = sha1_prefix.length
       val m = l + SHA1.digest_length
-      val n = heap.file.length
+      val n = File.size(heap)
       val bs = Bytes.read_file(heap, offset = n - m)
       if (bs.length == m) {
         val s = bs.text
diff -r 932b2a7139e2 -r c125f75a5144 src/Pure/Tools/profiling.scala
--- a/src/Pure/Tools/profiling.scala	Sun Nov 12 12:33:22 2023 +0100
+++ b/src/Pure/Tools/profiling.scala	Sun Nov 12 12:34:04 2023 +0100
@@ -97,7 +97,7 @@
         locales = session.locales,
         locale_thms = session.locale_thms,
         global_thms = session.global_thms,
-        heap_size = Space.bytes(store.the_heap(session_name).file.length),
+        heap_size = File.space(store.the_heap(session_name)),
         thys_id_size = session.sizeof_thys_id,
         thms_id_size = session.sizeof_thms_id,
         terms_size = session.sizeof_terms,