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