src/Tools/jEdit/src/plugin.scala
changeset 64818 67a0a563d2b3
parent 64817 0bb6b582bb4f
child 64835 fd1efd6dd385
--- a/src/Tools/jEdit/src/plugin.scala	Sat Jan 07 14:34:53 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Sat Jan 07 15:16:36 2017 +0100
@@ -322,13 +322,11 @@
             JEdit_Sessions.session_info().open_root).foreach(_.follow(view))
 
         case msg: BufferUpdate
-        if msg.getWhat == BufferUpdate.LOADED ||
-          msg.getWhat == BufferUpdate.PROPERTIES_CHANGED ||
-          msg.getWhat == BufferUpdate.CLOSING =>
+        if msg.getWhat == BufferUpdate.LOAD_STARTED || msg.getWhat == BufferUpdate.CLOSING =>
+          if (msg.getBuffer != null) PIDE.exit_models(List(msg.getBuffer))
 
-          if (msg.getWhat == BufferUpdate.CLOSING && msg.getBuffer != null)
-            PIDE.exit_models(List(msg.getBuffer))
-
+        case msg: BufferUpdate
+        if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED || msg.getWhat == BufferUpdate.LOADED =>
           if (PIDE.session.is_ready) {
             delay_init.invoke()
             delay_load.invoke()