need to handle EditPaneUpdate.CREATED explicitly, not included in EditPaneUpdate.BUFFER_CHANGED;
authorwenzelm
Tue, 15 Dec 2009 20:15:54 +0100
changeset 34787 0feac35069c6
parent 34786 7075919e4b96
child 34788 3779c54a2d21
need to handle EditPaneUpdate.CREATED explicitly, not included in EditPaneUpdate.BUFFER_CHANGED; tuned;
src/Tools/jEdit/src/jedit/plugin.scala
--- a/src/Tools/jEdit/src/jedit/plugin.scala	Tue Dec 15 19:53:35 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Tue Dec 15 20:15:54 2009 +0100
@@ -143,19 +143,22 @@
         val buffer = edit_pane.getBuffer
         val text_area = edit_pane.getTextArea
 
+        def init_view()
+        {
+          Document_Model.get(buffer) match {
+            case Some(model) => Document_View.init(model, text_area)
+            case None =>
+          }
+        }
+        def exit_view()
+        {
+          if (Document_View.get(text_area).isDefined)
+            Document_View.exit(text_area)
+        }
         msg.getWhat match {
-          case EditPaneUpdate.BUFFER_CHANGED =>
-            if (Document_View.get(text_area).isDefined)
-              Document_View.exit(text_area)
-            Document_Model.get(buffer) match {
-              case Some(model) => Document_View.init(model, text_area)
-              case None =>
-            }
-
-          case EditPaneUpdate.DESTROYED =>
-            if (Document_View.get(text_area).isDefined)
-              Document_View.exit(text_area)
-
+          case EditPaneUpdate.BUFFER_CHANGED => exit_view(); init_view()
+          case EditPaneUpdate.CREATED => init_view()
+          case EditPaneUpdate.DESTROYED => exit_view()
           case _ =>
         }