more robust shutdown, e.g. when plugin is stopped;

--- a/src/Tools/jEdit/src/jedit_editor.scala	Sun Aug 20 14:03:23 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Sun Aug 20 18:30:20 2017 +0200
@@ -39,6 +39,13 @@
   def invoke(): Unit = delay1_flush.invoke()
   def invoke_generated(): Unit = { delay1_flush.invoke(); delay2_flush.invoke() }
 
+  def shutdown(): Unit =
+    GUI_Thread.require {
+      delay1_flush.revoke()
+      delay2_flush.revoke()
+      Document_Model.flush_edits(hidden = false, purge = false)
+    }
+
   def visible_node(name: Document.Node.Name): Boolean =
     (for {
       text_area <- JEdit_Lib.jedit_text_areas()

--- a/src/Tools/jEdit/src/plugin.scala	Sun Aug 20 14:03:23 2017 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Sun Aug 20 18:30:20 2017 +0200
@@ -211,7 +211,7 @@
       GUI_Thread.later {
         delay_load.revoke()
         delay_init.revoke()
-        PIDE.editor.flush()
+        PIDE.editor.shutdown()
         exit_models(JEdit_Lib.jedit_buffers().toList)
       }
 
@@ -454,5 +454,6 @@
     exit_models(JEdit_Lib.jedit_buffers().toList)
     session.stop()
     file_watcher.shutdown()
+    PIDE.editor.shutdown()
   }
 }