refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
--- 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)
--- 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