src/Tools/jEdit/src/plugin.scala
changeset 54461 6c360a6ade0e
parent 54326 c5556b404902
child 54509 1f77110c94ef
--- a/src/Tools/jEdit/src/plugin.scala	Sun Nov 17 09:30:13 2013 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Sun Nov 17 16:02:06 2013 +0100
@@ -80,6 +80,7 @@
   def exit_models(buffers: List[Buffer])
   {
     Swing_Thread.now {
+      PIDE.editor.flush()
       buffers.foreach(buffer =>
         JEdit_Lib.buffer_lock(buffer) {
           JEdit_Lib.jedit_text_areas(buffer).foreach(Document_View.exit)
@@ -91,6 +92,7 @@
   def init_models(buffers: List[Buffer])
   {
     Swing_Thread.now {
+      PIDE.editor.flush()
       val init_edits =
         (List.empty[Document.Edit_Text] /: buffers) { case (edits, buffer) =>
           JEdit_Lib.buffer_lock(buffer) {