# HG changeset patch
# User wenzelm
# Date 1277585065 -7200
# Node ID 1ae272fd4082fe82eeb01fc3dac07caa01d3f24f
# Parent  2bf29095d26fdc8031d1c18b5572efef245bf1e2
refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;

diff -r 2bf29095d26f -r 1ae272fd4082 src/Tools/jEdit/src/jedit/document_model.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala	Sat Jun 26 22:19:55 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Sat Jun 26 22:44:25 2010 +0200
@@ -140,9 +140,11 @@
 
   /* activation */
 
+  private val token_marker = new Isabelle_Token_Marker(this)
+
   def activate()
   {
-    buffer.setTokenMarker(new Isabelle_Token_Marker(this))
+    buffer.setTokenMarker(token_marker)
     buffer.addBufferListener(buffer_listener)
     buffer.propertiesChanged()
 
@@ -150,6 +152,11 @@
     edits_delay()
   }
 
+  def refresh()
+  {
+    buffer.setTokenMarker(token_marker)
+  }
+
   def deactivate()
   {
     buffer.setTokenMarker(buffer.getMode.getTokenMarker)
diff -r 2bf29095d26f -r 1ae272fd4082 src/Tools/jEdit/src/jedit/plugin.scala
--- a/src/Tools/jEdit/src/jedit/plugin.scala	Sat Jun 26 22:19:55 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Sat Jun 26 22:44:25 2010 +0200
@@ -20,7 +20,7 @@
 import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View}
 import org.gjt.sp.jedit.buffer.JEditBuffer
 import org.gjt.sp.jedit.textarea.JEditTextArea
-import org.gjt.sp.jedit.msg.{EditPaneUpdate, PropertiesChanged}
+import org.gjt.sp.jedit.msg.{BufferUpdate, EditPaneUpdate, PropertiesChanged}
 import org.gjt.sp.jedit.gui.DockableWindowManager
 
 
@@ -203,6 +203,13 @@
   override def handleMessage(message: EBMessage)
   {
     message match {
+      case msg: BufferUpdate
+        if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
+        Document_Model(msg.getBuffer) match {
+          case Some(model) => model.refresh()
+          case _ =>
+        }
+
       case msg: EditPaneUpdate =>
         val edit_pane = msg.getEditPane
         val buffer = edit_pane.getBuffer