# HG changeset patch
# User wenzelm
# Date 1699788368 -3600
# Node ID 12abaffb0346046b169590e7f6a3b1d0acc2ec6b
# Parent  db9dba720ac7d5de9da13a1c997563d71d04c688
tuned signature: more operations;

diff -r db9dba720ac7 -r 12abaffb0346 src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Sat Nov 11 22:17:14 2023 +0100
+++ b/src/Pure/Admin/build_history.scala	Sun Nov 12 12:26:08 2023 +0100
@@ -357,7 +357,7 @@
         build_info.finished_sessions.flatMap { session_name =>
           val heap = isabelle_output + Path.explode(session_name)
           if (heap.is_file) {
-            Some("Heap " + session_name + " (" + Value.Long(File.space(heap).bytes) + " bytes)")
+            Some("Heap " + session_name + " (" + Value.Long(File.size(heap)) + " bytes)")
           }
           else None
         }
diff -r db9dba720ac7 -r 12abaffb0346 src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Sat Nov 11 22:17:14 2023 +0100
+++ b/src/Pure/General/bytes.scala	Sun Nov 12 12:26:08 2023 +0100
@@ -73,7 +73,7 @@
   def read_url(name: String): Bytes = using(Url(name).openStream)(read_stream(_))
 
   def read_file(path: Path, offset: Long = 0L, limit: Long = Long.MaxValue): Bytes = {
-    val length = File.space(path).bytes
+    val length = File.size(path)
     val start = offset.max(0L)
     val len = (length - start).max(0L).min(limit)
     if (len > Int.MaxValue) error("Cannot read large file slice: " + Space.bytes(len).print)
diff -r db9dba720ac7 -r 12abaffb0346 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Sat Nov 11 22:17:14 2023 +0100
+++ b/src/Pure/General/file.scala	Sun Nov 12 12:26:08 2023 +0100
@@ -408,8 +408,8 @@
   }
 
 
-  /* space */
+  /* strict file size */
 
-  def space(path: Path): Space =
-    Space.bytes(path.check_file.file.length)
+  def size(path: Path): Long = path.check_file.file.length
+  def space(path: Path): Space = Space.bytes(size(path))
 }
diff -r db9dba720ac7 -r 12abaffb0346 src/Pure/ML/ml_heap.scala
--- a/src/Pure/ML/ml_heap.scala	Sat Nov 11 22:17:14 2023 +0100
+++ b/src/Pure/ML/ml_heap.scala	Sun Nov 12 12:26:08 2023 +0100
@@ -151,7 +151,7 @@
     database match {
       case None =>
       case Some(db) =>
-        val size = File.space(heap).bytes - sha1_prefix.length - SHA1.digest_length
+        val size = File.size(heap) - sha1_prefix.length - SHA1.digest_length
 
         val slices = (size.toDouble / slice.toDouble).ceil.toInt
         val step = (size.toDouble / slices.toDouble).ceil.toLong
diff -r db9dba720ac7 -r 12abaffb0346 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Sat Nov 11 22:17:14 2023 +0100
+++ b/src/Pure/PIDE/headless.scala	Sun Nov 12 12:26:08 2023 +0100
@@ -92,7 +92,7 @@
       def finished: Load_State = Load_State(Nil, Nil, Space.zero)
 
       def count_file(name: Document.Node.Name): Long =
-        if (loaded_theory(name)) 0 else File.space(name.path).bytes
+        if (loaded_theory(name)) 0 else File.size(name.path)
     }
 
     private case class Load_State(