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)
 }