# HG changeset patch
# User wenzelm
# Date 1483893360 -3600
# Node ID ae6c51dcba9c643e56fada1cd6c1fa0b915dd1c2
# Parent  4efe34df91369cca72dd4f91619e340598010e17
avoid immediate editor.flush on buffer events;

diff -r 4efe34df9136 -r ae6c51dcba9c src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Sun Jan 08 17:22:14 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Sun Jan 08 17:36:00 2017 +0100
@@ -74,7 +74,6 @@
   def exit_models(buffers: List[Buffer])
   {
     GUI_Thread.now {
-      PIDE.editor.flush()
       buffers.foreach(buffer =>
         JEdit_Lib.buffer_lock(buffer) {
           JEdit_Lib.jedit_text_areas(buffer).foreach(Document_View.exit)
@@ -270,6 +269,8 @@
       case Session.Shutdown =>
         GUI_Thread.later {
           delay_load.revoke()
+          delay_init.revoke()
+          PIDE.editor.flush()
           PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
         }
 
@@ -314,7 +315,10 @@
 
         case msg: BufferUpdate
         if msg.getWhat == BufferUpdate.LOAD_STARTED || msg.getWhat == BufferUpdate.CLOSING =>
-          if (msg.getBuffer != null) PIDE.exit_models(List(msg.getBuffer))
+          if (msg.getBuffer != null) {
+            PIDE.exit_models(List(msg.getBuffer))
+            PIDE.editor.invoke_generated()
+          }
 
         case msg: BufferUpdate
         if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED || msg.getWhat == BufferUpdate.LOADED =>