need to handle EditPaneUpdate.CREATED explicitly, not included in EditPaneUpdate.BUFFER_CHANGED;
tuned;
--- 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 _ =>
}