src/Tools/jEdit/src/jedit_editor.scala

--- 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()