# HG changeset patch
# User wenzelm
# Date 1674830001 -3600
# Node ID e3a2b3536030a123a6de60aa6a4ff7d80ac39e73
# Parent  4f68b165d69e6eb8bfa1d5d35f325006238e0d2a
prefer typed bytes count, but retain toString of original Long for robustness of Java/Scala string composition;

diff -r 4f68b165d69e -r e3a2b3536030 etc/build.props
--- a/etc/build.props	Fri Jan 27 15:22:26 2023 +0100
+++ b/etc/build.props	Fri Jan 27 15:33:21 2023 +0100
@@ -96,6 +96,7 @@
   src/Pure/General/rsync.scala \
   src/Pure/General/scan.scala \
   src/Pure/General/sha1.scala \
+  src/Pure/General/space.scala \
   src/Pure/General/sql.scala \
   src/Pure/General/ssh.scala \
   src/Pure/General/symbol.scala \
diff -r 4f68b165d69e -r e3a2b3536030 src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Fri Jan 27 15:22:26 2023 +0100
+++ b/src/Pure/Admin/build_history.scala	Fri Jan 27 15:33:21 2023 +0100
@@ -346,7 +346,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(heap.file.length) + " bytes)")
+            Some("Heap " + session_name + " (" + Value.Long(File.space(heap).bytes) + " bytes)")
           }
           else None
         }
diff -r 4f68b165d69e -r e3a2b3536030 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Fri Jan 27 15:22:26 2023 +0100
+++ b/src/Pure/General/file.scala	Fri Jan 27 15:33:21 2023 +0100
@@ -399,4 +399,10 @@
 
     def output(out: XML.Body => String): Content = new Content(path, Bytes(out(content)))
   }
+
+
+  /* space */
+
+  def space(path: Path): Space =
+    Space.bytes(path.file.length)
 }
diff -r 4f68b165d69e -r e3a2b3536030 src/Pure/General/space.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/space.scala	Fri Jan 27 15:33:21 2023 +0100
@@ -0,0 +1,17 @@
+/*  Title:      Pure/General/space.scala
+    Author:     Makarius
+
+Storage space based on bytes.
+*/
+
+package isabelle
+
+
+object Space {
+  def bytes(bs: Long): Space = new Space(bs)
+  val zero: Space = bytes(0L)
+}
+
+final class Space private(val bytes: Long) extends AnyVal {
+  override def toString: String = bytes.toString
+}