--- 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