# HG changeset patch
# User wenzelm
# Date 1260904554 -3600
# Node ID 0feac35069c67cd9fa96780b7965881703c9dc28
# Parent  7075919e4b9691ce79cac5f04b3cff39bacc820d
need to handle EditPaneUpdate.CREATED explicitly, not included in EditPaneUpdate.BUFFER_CHANGED;
tuned;

diff -r 7075919e4b96 -r 0feac35069c6 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 _ =>
         }