# HG changeset patch # User wenzelm # Date 1571085463 -7200 # Node ID b627cfb23595869614360e1293b38ce4a0b96a17 # Parent 7c77fb7a6fc96117c03cf04c562f54b709f6261c clarified count_file; diff -r 7c77fb7a6fc9 -r b627cfb23595 src/Pure/PIDE/headless.scala --- a/src/Pure/PIDE/headless.scala Mon Oct 14 22:34:33 2019 +0200 +++ b/src/Pure/PIDE/headless.scala Mon Oct 14 22:37:43 2019 +0200 @@ -92,7 +92,7 @@ def finished: Load_State = Load_State(Nil, Nil, 0) def count_file(name: Document.Node.Name): Long = - name.path.file.length + if (loaded_theory(name)) 0 else name.path.file.length } private case class Load_State(