--- 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)