tuned whitespace;
authorwenzelm
Thu, 08 Dec 2022 21:41:26 +0100
changeset 76607 1a56906176fb
parent 76606 3558388330f8
child 76608 16f049023619
tuned whitespace;
src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Thu Dec 08 17:23:31 2022 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Thu Dec 08 21:41:26 2022 +0100
@@ -457,7 +457,7 @@
   def flush_edits(
     doc_blobs: Document.Blobs,
     hidden: Boolean
-  ) : Option[(List[Document.Edit_Text], File_Model)] = {
+  ): Option[(List[Document.Edit_Text], File_Model)] = {
     val (reparse, perspective) = node_perspective(doc_blobs, hidden)
     if (reparse || pending_edits.nonEmpty || last_perspective != perspective) {
       val edits = node_edits(node_header, pending_edits, perspective)