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