src/Tools/jEdit/src/jedit/plugin.scala
changeset 37557 1ae272fd4082
parent 37241 04d2521e79b0
child 38221 e0f00f0945b4
--- 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