changeset 76714 | 95a926d483c5 |
parent 75393 | 87ebf5a50283 |
child 76716 | a7602257a825 |
--- a/src/Pure/PIDE/document_status.scala Mon Dec 19 14:39:22 2022 +0100 +++ b/src/Pure/PIDE/document_status.scala Mon Dec 19 15:29:24 2022 +0100 @@ -100,7 +100,8 @@ def make( state: Document.State, version: Document.Version, - name: Document.Node.Name): Node_Status = { + name: Document.Node.Name + ): Node_Status = { val node = version.nodes(name) var unprocessed = 0