# HG changeset patch
# User wenzelm
# Date 1730725821 -3600
# Node ID 2176778f9ed7a1be72d934abfe2bac9e91437384
# Parent  40af19b10f8a1f169fd593777edc478cb140145f
proper parentheses, for the sake of IntelliJ IDEA;

diff -r 40af19b10f8a -r 2176778f9ed7 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Mon Nov 04 12:58:05 2024 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Nov 04 14:10:21 2024 +0100
@@ -228,7 +228,7 @@
   def flush_edits(hidden: Boolean, purge: Boolean): (Document.Blobs, List[Document.Edit_Text]) = {
     GUI_Thread.require {}
 
-    state.change_result { st =>
+    state.change_result({ st =>
       val doc_blobs = st.document_blobs
 
       val buffer_edits =
@@ -273,7 +273,7 @@
         } yield file.getParentFile).toSet)
 
       ((doc_blobs, model_edits ::: purge_edits), st1)
-    }
+    })
   }