author | wenzelm |
Mon, 19 Dec 2022 15:29:24 +0100 | |
changeset 76714 | 95a926d483c5 |
parent 76713 | d8b3b8a179c2 |
child 76715 | bf5ff407f32f |
--- 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