centralized management of pending buffer edits;

--- a/src/Pure/PIDE/editor.scala	Sun Nov 17 09:30:13 2013 +0100
+++ b/src/Pure/PIDE/editor.scala	Sun Nov 17 16:02:06 2013 +0100
@@ -11,6 +11,7 @@
 {
   def session: Session
   def flush(): Unit
+  def invoke(): Unit
   def current_context: Context
   def current_node(context: Context): Option[Document.Node.Name]
   def current_node_snapshot(context: Context): Option[Document.Snapshot]

--- a/src/Tools/jEdit/src/document_model.scala	Sun Nov 17 09:30:13 2013 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Sun Nov 17 16:02:06 2013 +0100
@@ -124,16 +124,23 @@
       node_name -> perspective)
   }
 
-  def node_edits(perspective: Document.Node.Perspective_Text, text_edits: List[Text.Edit])
-    : List[Document.Edit_Text] =
+  def node_edits(
+    clear: Boolean,
+    text_edits: List[Text.Edit],
+    perspective: Document.Node.Perspective_Text): List[Document.Edit_Text] =
   {
     Swing_Thread.require()
 
-    val header = node_header()
-
-    List(session.header_edit(node_name, header),
-      node_name -> Document.Node.Edits(text_edits),
-      node_name -> perspective)
+    val header_edit = session.header_edit(node_name, node_header())
+    if (clear)
+      List(header_edit,
+        node_name -> Document.Node.Clear(),
+        node_name -> Document.Node.Edits(text_edits),
+        node_name -> perspective)
+    else
+      List(header_edit,
+        node_name -> Document.Node.Edits(text_edits),
+        node_name -> perspective)
   }
 
 
@@ -141,6 +148,7 @@
 
   private object pending_edits  // owned by Swing thread
   {
+    private var pending_clear = false
     private val pending = new mutable.ListBuffer[Text.Edit]
     private var last_perspective = empty_perspective
 
@@ -150,45 +158,33 @@
     {
       Swing_Thread.require()
 
+      val clear = pending_clear
       val edits = snapshot()
-      val new_perspective = node_perspective()
-      if (!edits.isEmpty || last_perspective != new_perspective) {
+      val perspective = node_perspective()
+      if (clear || !edits.isEmpty || last_perspective != perspective) {
+        pending_clear = false
         pending.clear
-        last_perspective = new_perspective
-        node_edits(new_perspective, edits)
+        last_perspective = perspective
+        node_edits(clear, edits, perspective)
       }
       else Nil
     }
 
-    def flush(): Unit = session.update(flushed_edits())
-
-    val delay_flush =
-      Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
-
-    def +=(edit: Text.Edit)
+    def edit(clear: Boolean, e: Text.Edit)
     {
       Swing_Thread.require()
-      pending += edit
-      delay_flush.invoke()
-    }
 
-    def init()
-    {
-      flush()
-      session.update(init_edits())
-    }
-
-    def exit()
-    {
-      delay_flush.revoke()
-      flush()
+      if (clear) {
+        pending_clear = true
+        pending.clear
+      }
+      pending += e
+      PIDE.editor.invoke()
     }
   }
 
   def flushed_edits(): List[Document.Edit_Text] = pending_edits.flushed_edits()
 
-  def update_perspective(): Unit = pending_edits.delay_flush.invoke()
-
 
   /* snapshot */
 
@@ -205,21 +201,21 @@
   {
     override def bufferLoaded(buffer: JEditBuffer)
     {
-      pending_edits.init()
+      pending_edits.edit(true, Text.Edit.insert(0, buffer.getText(0, buffer.getLength)))
     }
 
     override def contentInserted(buffer: JEditBuffer,
       start_line: Int, offset: Int, num_lines: Int, length: Int)
     {
       if (!buffer.isLoading)
-        pending_edits += Text.Edit.insert(offset, buffer.getText(offset, length))
+        pending_edits.edit(false, Text.Edit.insert(offset, buffer.getText(offset, length)))
     }
 
     override def preContentRemoved(buffer: JEditBuffer,
       start_line: Int, offset: Int, num_lines: Int, removed_length: Int)
     {
       if (!buffer.isLoading)
-        pending_edits += Text.Edit.remove(offset, buffer.getText(offset, removed_length))
+        pending_edits.edit(false, Text.Edit.remove(offset, buffer.getText(offset, removed_length)))
     }
   }
 
@@ -229,13 +225,11 @@
   private def activate()
   {
     buffer.addBufferListener(buffer_listener)
-    pending_edits.flush()
     Token_Markup.refresh_buffer(buffer)
   }
 
   private def deactivate()
   {
-    pending_edits.exit()
     buffer.removeBufferListener(buffer_listener)
     Token_Markup.refresh_buffer(buffer)
   }

--- a/src/Tools/jEdit/src/document_view.scala	Sun Nov 17 09:30:13 2013 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Sun Nov 17 16:02:06 2013 +0100
@@ -106,14 +106,14 @@
     Text.Perspective(active_command ::: visible_lines)
   }
 
-  private def update_perspective = new TextAreaExtension
+  private def update_view = new TextAreaExtension
   {
     override def paintScreenLineRange(gfx: Graphics2D,
       first_line: Int, last_line: Int, physical_lines: Array[Int],
       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     {
       // no robust_body
-      model.update_perspective()
+      PIDE.editor.invoke()
     }
   }
 
@@ -251,7 +251,7 @@
   {
     val painter = text_area.getPainter
 
-    painter.addExtension(TextAreaPainter.LOWEST_LAYER, update_perspective)
+    painter.addExtension(TextAreaPainter.LOWEST_LAYER, update_view)
     rich_text_area.activate()
     text_area.getGutter.addExtension(gutter_painter)
     text_area.addKeyListener(key_listener)
@@ -272,6 +272,6 @@
     text_area.removeKeyListener(key_listener)
     text_area.getGutter.removeExtension(gutter_painter)
     rich_text_area.deactivate()
-    painter.removeExtension(update_perspective)
+    painter.removeExtension(update_view)
   }
 }

--- a/src/Tools/jEdit/src/jedit_editor.scala	Sun Nov 17 09:30:13 2013 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Sun Nov 17 16:02:06 2013 +0100
@@ -36,6 +36,11 @@
     )
   }
 
+  private val delay_flush =
+    Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
+
+  def invoke(): Unit = Swing_Thread.require { delay_flush.invoke() }
+
 
   /* current situation */
 

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