src/Pure/PIDE/document_status.scala
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