tuned whitespace;
authorwenzelm
Mon, 19 Dec 2022 15:29:24 +0100
changeset 76714 95a926d483c5
parent 76713 d8b3b8a179c2
child 76715 bf5ff407f32f
tuned whitespace;
src/Pure/PIDE/document_status.scala
--- 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