# HG changeset patch
# User wenzelm
# Date 1289490526 -3600
# Node ID 4bae781b8f7c34fc5ea07da720085291393f9213
# Parent  780c272765931f12640616b962a140a8065380bb
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
Document_Model.pending_edits: more robust treatment of init, including buffer reload event (jEdit 4.3.2 produces malformed remove/insert that lacks the last character);
tuned;

diff -r 780c27276593 -r 4bae781b8f7c src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Thu Nov 11 13:23:39 2010 +0100
+++ b/src/Pure/PIDE/document.scala	Thu Nov 11 16:48:46 2010 +0100
@@ -17,7 +17,8 @@
 
   type ID = Long
 
-  object ID {
+  object ID
+  {
     def apply(id: ID): String = Markup.Long.apply(id)
     def unapply(s: String): Option[ID] = Markup.Long.unapply(s)
   }
@@ -34,7 +35,9 @@
 
   /* named nodes -- development graph */
 
-  type Node_Text_Edit = (String, List[Text.Edit])  // FIXME None: remove
+  type Text_Edit =
+   (String,  // node name
+    Option[List[Text.Edit]])  // None: remove, Some: insert/remove text
 
   type Edit[C] =
    (String,  // node name
@@ -133,7 +136,7 @@
 
   class Change(
     val previous: Future[Version],
-    val edits: List[Node_Text_Edit],
+    val edits: List[Text_Edit],
     val result: Future[(List[Edit[Command]], Version)])
   {
     val version: Future[Version] = result.map(_._2)
@@ -267,7 +270,7 @@
       }
 
     def extend_history(previous: Future[Version],
-        edits: List[Node_Text_Edit],
+        edits: List[Text_Edit],
         result: Future[(List[Edit[Command]], Version)]): (Change, State) =
     {
       val change = new Change(previous, edits, result)
@@ -284,9 +287,10 @@
       val stable = found_stable.get
       val latest = history.undo_list.head
 
+      // FIXME proper treatment of deleted nodes
       val edits =
         (pending_edits /: history.undo_list.takeWhile(_ != stable))((edits, change) =>
-            (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
+            (for ((a, Some(eds)) <- change.edits if a == name) yield eds).flatten ::: edits)
       lazy val reverse_edits = edits.reverse
 
       new Snapshot
diff -r 780c27276593 -r 4bae781b8f7c src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Thu Nov 11 13:23:39 2010 +0100
+++ b/src/Pure/System/session.scala	Thu Nov 11 16:48:46 2010 +0100
@@ -135,7 +135,7 @@
   def current_state(): Document.State = global_state.peek()
 
   private case object Interrupt_Prover
-  private case class Edit_Version(edits: List[Document.Node_Text_Edit])
+  private case class Edit_Version(edits: List[Document.Text_Edit])
   private case class Start(timeout: Int, args: List[String])
 
   private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
@@ -289,7 +289,7 @@
 
   def interrupt() { session_actor ! Interrupt_Prover }
 
-  def edit_version(edits: List[Document.Node_Text_Edit]) { session_actor !? Edit_Version(edits) }
+  def edit_version(edits: List[Document.Text_Edit]) { session_actor !? Edit_Version(edits) }
 
   def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
     global_state.peek().snapshot(name, pending_edits)
diff -r 780c27276593 -r 4bae781b8f7c src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Thu Nov 11 13:23:39 2010 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Thu Nov 11 16:48:46 2010 +0100
@@ -17,10 +17,7 @@
 
   object Structure
   {
-    sealed abstract class Entry
-    {
-      def length: Int
-    }
+    sealed abstract class Entry { def length: Int }
     case class Block(val name: String, val body: List[Entry]) extends Entry
     {
       val length: Int = (0 /: body)(_ + _.length)
@@ -103,7 +100,7 @@
   /** text edits **/
 
   def text_edits(session: Session, previous: Document.Version,
-      edits: List[Document.Node_Text_Edit]): (List[Document.Edit[Command]], Document.Version) =
+      edits: List[Document.Text_Edit]): (List[Document.Edit[Command]], Document.Version) =
   {
     /* phase 1: edit individual command source */
 
@@ -178,20 +175,25 @@
       val doc_edits = new mutable.ListBuffer[Document.Edit[Command]]
       var nodes = previous.nodes
 
-      for ((name, text_edits) <- edits) {
-        val commands0 = nodes(name).commands
-        val commands1 = edit_text(text_edits, commands0)
-        val commands2 = recover_spans(commands1)   // FIXME somewhat slow
+      edits foreach {
+        case (name, None) =>
+          doc_edits += (name -> None)
+          nodes -= name
+
+        case (name, Some(text_edits)) =>
+          val commands0 = nodes(name).commands
+          val commands1 = edit_text(text_edits, commands0)
+          val commands2 = recover_spans(commands1)   // FIXME somewhat slow
 
-        val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
-        val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList
+          val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
+          val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList
 
-        val cmd_edits =
-          removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
-          inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
+          val cmd_edits =
+            removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
+            inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
 
-        doc_edits += (name -> Some(cmd_edits))
-        nodes += (name -> new Document.Node(commands2))
+          doc_edits += (name -> Some(cmd_edits))
+          nodes += (name -> new Document.Node(commands2))
       }
       (doc_edits.toList, new Document.Version(session.new_id(), nodes))
     }
diff -r 780c27276593 -r 4bae781b8f7c src/Tools/jEdit/src/jedit/document_model.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala	Thu Nov 11 13:23:39 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Thu Nov 11 16:48:46 2010 +0100
@@ -116,18 +116,25 @@
     private val pending = new mutable.ListBuffer[Text.Edit]
     def snapshot(): List[Text.Edit] = pending.toList
 
-    private val delay_flush = Swing_Thread.delay_last(session.input_delay) {
-      if (!pending.isEmpty) session.edit_version(List((thy_name, flush())))
-    }
-
-    def flush(): List[Text.Edit] =
+    def flush(more_edits: Option[List[Text.Edit]]*)
     {
       Swing_Thread.require()
       val edits = snapshot()
       pending.clear
-      edits
+
+      if (!edits.isEmpty || !more_edits.isEmpty)
+        session.edit_version((Some(edits) :: more_edits.toList).map((thy_name, _)))
     }
 
+    def init()
+    {
+      Swing_Thread.require()
+      flush(None, Some(List(Text.Edit.insert(0, Isabelle.buffer_text(buffer)))))
+    }
+
+    private val delay_flush =
+      Swing_Thread.delay_last(session.input_delay) { flush() }
+
     def +=(edit: Text.Edit)
     {
       Swing_Thread.require()
@@ -150,16 +157,23 @@
 
   private val buffer_listener: BufferListener = new BufferAdapter
   {
+    override def bufferLoaded(buffer: JEditBuffer)
+    {
+      pending_edits.init()
+    }
+
     override def contentInserted(buffer: JEditBuffer,
       start_line: Int, offset: Int, num_lines: Int, length: Int)
     {
-      pending_edits += Text.Edit.insert(offset, buffer.getText(offset, length))
+      if (!buffer.isLoading)
+        pending_edits += Text.Edit.insert(offset, buffer.getText(offset, length))
     }
 
     override def preContentRemoved(buffer: JEditBuffer,
       start_line: Int, offset: Int, num_lines: Int, removed_length: Int)
     {
-      pending_edits += Text.Edit.remove(offset, buffer.getText(offset, removed_length))
+      if (!buffer.isLoading)
+        pending_edits += Text.Edit.remove(offset, buffer.getText(offset, removed_length))
     }
   }
 
@@ -219,7 +233,7 @@
     buffer.setTokenMarker(token_marker)
     buffer.addBufferListener(buffer_listener)
     buffer.propertiesChanged()
-    pending_edits += Text.Edit.insert(0, Isabelle.buffer_text(buffer))
+    pending_edits.init()
   }
 
   def refresh()
@@ -229,6 +243,7 @@
 
   def deactivate()
   {
+    pending_edits.flush()
     buffer.setTokenMarker(buffer.getMode.getTokenMarker)
     buffer.removeBufferListener(buffer_listener)
   }