clarified buffer events: exit model while loading;
misc tuning;

--- a/src/Tools/jEdit/src/document_model.scala	Sat Jan 07 14:34:53 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Sat Jan 07 15:16:36 2017 +0100
@@ -279,11 +279,11 @@
         get_blob match {
           case None =>
             List(session.header_edit(node_name, node_header),
-              node_name -> Document.Node.Edits(pending_edits.toList),
+              node_name -> Document.Node.Edits(pending_edits),
               node_name -> perspective)
           case Some(blob) =>
             List(node_name -> Document.Node.Blob(blob),
-              node_name -> Document.Node.Edits(pending_edits.toList))
+              node_name -> Document.Node.Edits(pending_edits))
         }
       Some((edits, copy(last_perspective = perspective, pending_edits = Nil)))
     }
@@ -294,7 +294,7 @@
   /* snapshot */
 
   def is_stable: Boolean = pending_edits.isEmpty
-  def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits.toList)
+  def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits)
 }
 
 case class Buffer_Model(session: Session, node_name: Document.Node.Name, buffer: Buffer)
@@ -368,7 +368,7 @@
               _blob = Some((bytes, chunk))
               (bytes, chunk)
           }
-        val changed = pending_edits.is_pending()
+        val changed = pending_edits.nonEmpty
         Some(Document.Blob(bytes, chunk, changed))
       }
     }
@@ -398,24 +398,15 @@
 
   /* edits */
 
-  def node_edits(
-      clear: Boolean,
-      text_edits: List[Text.Edit],
-      perspective: Document.Node.Perspective_Text): List[Document.Edit_Text] =
+  def node_edits(text_edits: List[Text.Edit], perspective: Document.Node.Perspective_Text)
+    : List[Document.Edit_Text] =
   {
     val edits: List[Document.Edit_Text] =
       get_blob match {
         case None =>
-          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)
+          List(session.header_edit(node_name, node_header()),
+            node_name -> Document.Node.Edits(text_edits),
+            node_name -> perspective)
         case Some(blob) =>
           List(node_name -> Document.Node.Blob(blob),
             node_name -> Document.Node.Edits(text_edits))
@@ -428,12 +419,11 @@
 
   private object pending_edits
   {
-    private var pending_clear = false
     private val pending = new mutable.ListBuffer[Text.Edit]
     private var last_perspective = Document.Node.no_perspective_text
 
-    def is_pending(): Boolean = synchronized { pending_clear || pending.nonEmpty }
-    def get_edits(): List[Text.Edit] = synchronized { pending.toList }
+    def nonEmpty: Boolean = synchronized { pending.nonEmpty }
+    def get_edits: List[Text.Edit] = synchronized { pending.toList }
     def get_last_perspective: Document.Node.Perspective_Text = synchronized { last_perspective }
     def set_last_perspective(perspective: Document.Node.Perspective_Text): Unit =
       synchronized { last_perspective = perspective }
@@ -442,19 +432,17 @@
       synchronized {
         GUI_Thread.require {}
 
-        val clear = pending_clear
-        val edits = get_edits()
+        val edits = get_edits
         val (reparse, perspective) = node_perspective(doc_blobs, hidden)
-        if (clear || reparse || edits.nonEmpty || last_perspective != perspective) {
-          pending_clear = false
+        if (reparse || edits.nonEmpty || last_perspective != perspective) {
           pending.clear
           last_perspective = perspective
-          node_edits(clear, edits, perspective)
+          node_edits(edits, perspective)
         }
         else Nil
       }
 
-    def edit(clear: Boolean, e: Text.Edit): Unit = synchronized
+    def edit(edits: List[Text.Edit]): Unit = synchronized
     {
       GUI_Thread.require {}
 
@@ -464,17 +452,13 @@
       for (doc_view <- PIDE.document_views(buffer))
         doc_view.rich_text_area.active_reset()
 
-      if (clear) {
-        pending_clear = true
-        pending.clear
-      }
-      pending += e
+      pending ++= edits
       PIDE.editor.invoke()
     }
   }
 
-  def is_stable(): Boolean = !pending_edits.is_pending();
-  def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits.get_edits())
+  def is_stable(): Boolean = !pending_edits.nonEmpty
+  def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits.get_edits)
 
   def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] =
     pending_edits.flush_edits(doc_blobs, hidden)
@@ -484,23 +468,16 @@
 
   private val buffer_listener: BufferListener = new BufferAdapter
   {
-    override def bufferLoaded(buffer: JEditBuffer)
-    {
-      pending_edits.edit(true, Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer)))
-    }
-
     override def contentInserted(buffer: JEditBuffer,
       start_line: Int, offset: Int, num_lines: Int, length: Int)
     {
-      if (!buffer.isLoading)
-        pending_edits.edit(false, Text.Edit.insert(offset, buffer.getText(offset, length)))
+      pending_edits.edit(List(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.edit(false, Text.Edit.remove(offset, buffer.getText(offset, removed_length)))
+      pending_edits.edit(List(Text.Edit.remove(offset, buffer.getText(offset, removed_length))))
     }
   }
 
@@ -535,15 +512,13 @@
 
     old_model match {
       case None =>
-        pending_edits.edit(true, Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer)))
+        pending_edits.edit(List(Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer))))
       case Some(file_model) =>
         set_node_required(file_model.node_required)
         pending_edits.set_last_perspective(file_model.last_perspective)
-        for {
-          edit <-
-            file_model.pending_edits :::
-              Text.Edit.replace(0, file_model.content.text, JEdit_Lib.buffer_text(buffer))
-        } pending_edits.edit(false, edit)
+        pending_edits.edit(
+          file_model.pending_edits :::
+            Text.Edit.replace(0, file_model.content.text, JEdit_Lib.buffer_text(buffer)))
     }
 
     buffer.addBufferListener(buffer_listener)
@@ -564,6 +539,6 @@
 
     val content = Document_Model.File_Content(JEdit_Lib.buffer_text(buffer))
     File_Model(session, node_name, content, node_required,
-      pending_edits.get_last_perspective, pending_edits.get_edits())
+      pending_edits.get_last_perspective, pending_edits.get_edits)
   }
 }

--- a/src/Tools/jEdit/src/plugin.scala	Sat Jan 07 14:34:53 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Sat Jan 07 15:16:36 2017 +0100
@@ -322,13 +322,11 @@
             JEdit_Sessions.session_info().open_root).foreach(_.follow(view))
 
         case msg: BufferUpdate
-        if msg.getWhat == BufferUpdate.LOADED ||
-          msg.getWhat == BufferUpdate.PROPERTIES_CHANGED ||
-          msg.getWhat == BufferUpdate.CLOSING =>
+        if msg.getWhat == BufferUpdate.LOAD_STARTED || msg.getWhat == BufferUpdate.CLOSING =>
+          if (msg.getBuffer != null) PIDE.exit_models(List(msg.getBuffer))
 
-          if (msg.getWhat == BufferUpdate.CLOSING && msg.getBuffer != null)
-            PIDE.exit_models(List(msg.getBuffer))
-
+        case msg: BufferUpdate
+        if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED || msg.getWhat == BufferUpdate.LOADED =>
           if (PIDE.session.is_ready) {
             delay_init.invoke()
             delay_load.invoke()