# HG changeset patch
# User wenzelm
# Date 1670532086 -3600
# Node ID 1a56906176fb3598d55044c1b6dbf3f5cd093ae9
# Parent  3558388330f891392598ccb6444f926c55ba7cd4
tuned whitespace;

diff -r 3558388330f8 -r 1a56906176fb 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)