# HG changeset patch
# User wenzelm
# Date 1671460164 -3600
# Node ID 95a926d483c54362f9e419833f114f1da5521dab
# Parent  d8b3b8a179c250eaba0412cb51416cfb16635b63
tuned whitespace;

diff -r d8b3b8a179c2 -r 95a926d483c5 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