author | wenzelm |
Fri, 27 Jan 2023 16:48:19 +0100 | |
changeset 77112 | 6f2ddbff972c |
parent 77111 | aa359010d264 |
child 77113 | c301b97b4301 |
--- 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(