# HG changeset patch
# User wenzelm
# Date 1417533011 -3600
# Node ID cf255dc2b48fe281e41ca93f5e79dfaeb9f7b6e0
# Parent  7e0d3da6e6d8440c8a11af5fc16f342890740709
more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;

diff -r 7e0d3da6e6d8 -r cf255dc2b48f src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Tue Dec 02 14:16:56 2014 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Tue Dec 02 16:10:11 2014 +0100
@@ -15,7 +15,7 @@
 
 import org.gjt.sp.jedit.jEdit
 import org.gjt.sp.jedit.Buffer
-import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
+import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer, LineManager}
 
 
 object Document_Model
@@ -284,28 +284,42 @@
   }
 
 
-  /* activation */
+  /* syntax */
 
-  private def refresh_token_marker()
+  def syntax_changed()
+  {
+    Untyped.get(buffer, "lineMgr").asInstanceOf[LineManager].setFirstInvalidLineContext(0)
+    for (text_area <- JEdit_Lib.jedit_text_areas(buffer)) {
+      val c = Class.forName("org.gjt.sp.jedit.textarea.TextArea")
+      val m = c.getDeclaredMethod("foldStructureChanged")
+      m.setAccessible(true)
+      m.invoke(text_area)
+    }
+  }
+
+  private def init_token_marker()
   {
     Isabelle.buffer_token_marker(buffer) match {
       case Some(marker) if marker != buffer.getTokenMarker =>
-        buffer.setTokenMarker(jEdit.getMode("text").getTokenMarker)
         buffer.setTokenMarker(marker)
+        syntax_changed()
       case _ =>
     }
   }
 
+
+  /* activation */
+
   private def activate()
   {
     pending_edits.edit(true, Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer)))
     buffer.addBufferListener(buffer_listener)
-    refresh_token_marker()
+    init_token_marker()
   }
 
   private def deactivate()
   {
     buffer.removeBufferListener(buffer_listener)
-    refresh_token_marker()
+    init_token_marker()
   }
 }
diff -r 7e0d3da6e6d8 -r cf255dc2b48f src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Tue Dec 02 14:16:56 2014 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Tue Dec 02 16:10:11 2014 +0100
@@ -114,7 +114,15 @@
 
   override def commit(change: Session.Change)
   {
-    if (!change.syntax_changed.isEmpty) GUI_Thread.later { jEdit.propertiesChanged() }
+    if (!change.syntax_changed.isEmpty)
+      GUI_Thread.later {
+        val changed = change.syntax_changed.toSet
+        for {
+          buffer <- JEdit_Lib.jedit_buffers()
+          model <- PIDE.document_model(buffer)
+          if changed(model.node_name)
+        } model.syntax_changed()
+      }
     if (change.deps_changed && PIDE.options.bool("jedit_auto_load")) PIDE.deps_changed()
   }
 }