src/Tools/jEdit/src/jedit/Plugin.scala
changeset 34671 d179fcb04cbc
parent 34670 c99878d7bec7
child 34685 93f4978fe2a8
--- a/src/Tools/jEdit/src/jedit/Plugin.scala	Thu Aug 27 10:51:09 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/Plugin.scala	Thu Aug 27 10:51:09 2009 +0200
@@ -133,17 +133,16 @@
   override def handleMessage(msg: EBMessage)
   {
     msg match {
-      case epu: EditPaneUpdate => epu.getWhat match {
-        case EditPaneUpdate.BUFFER_CHANGED =>
-          val buffer = epu.getEditPane.getBuffer
-          (mapping get buffer) map (_.theory_view.activate)
-          buffer.propertiesChanged()
-        case EditPaneUpdate.BUFFER_CHANGING =>
-          val buffer = epu.getEditPane.getBuffer
-          if (buffer != null)
-            (mapping get buffer) map (_.theory_view.deactivate)
-        case _ =>
-      }
+      case epu: EditPaneUpdate =>
+        val buffer = epu.getEditPane.getBuffer
+        epu.getWhat match {
+          case EditPaneUpdate.BUFFER_CHANGED =>
+            (mapping get buffer) map (_.theory_view.activate)
+          case EditPaneUpdate.BUFFER_CHANGING =>
+            if (buffer != null)
+              (mapping get buffer) map (_.theory_view.deactivate)
+          case _ =>
+        }
       case _ =>
     }
   }