# HG changeset patch
# User wenzelm
# Date 1674834499 -3600
# Node ID 6f2ddbff972c13261a40441d7efdfa45c9a85d50
# Parent  aa359010d264895d60a357ee8f89b64f0ec6b833
prefer typed/strict operations;

diff -r aa359010d264 -r 6f2ddbff972c src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Fri Jan 27 16:18:36 2023 +0100
+++ b/src/Pure/PIDE/headless.scala	Fri Jan 27 16:48:19 2023 +0100
@@ -90,7 +90,7 @@
       def finished: Load_State = Load_State(Nil, Nil, 0)
 
       def count_file(name: Document.Node.Name): Long =
-        if (loaded_theory(name)) 0 else name.path.file.length
+        if (loaded_theory(name)) 0 else File.space(name.path).bytes
     }
 
     private case class Load_State(