tuned;
authorwenzelm
Fri, 23 Dec 2022 15:34:09 +0100
changeset 76762 bb705a68b471
parent 76761 d062c7f4f2d1
child 76763 e9c48303ed11
tuned;
src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Fri Dec 23 15:29:29 2022 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Fri Dec 23 15:34:09 2022 +0100
@@ -601,8 +601,9 @@
       reset_blob()
       reset_bibtex_entries()
 
-      for (doc_view <- document_view_iterator)
+      for (doc_view <- document_view_iterator) {
         doc_view.rich_text_area.active_reset()
+      }
 
       pending ++= edits
       PIDE.editor.invoke()
@@ -646,9 +647,10 @@
 
   def syntax_changed(): Unit = {
     JEdit_Lib.buffer_line_manager(buffer).setFirstInvalidLineContext(0)
-    for (text_area <- JEdit_Lib.jedit_text_areas(buffer))
+    for (text_area <- JEdit_Lib.jedit_text_areas(buffer)) {
       Untyped.method(Class.forName("org.gjt.sp.jedit.textarea.TextArea"), "foldStructureChanged").
         invoke(text_area)
+    }
     buffer.invalidateCachedFoldLevels()
   }