src/Pure/PIDE/document.scala

 {
   /* formal identifiers */
 
   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)
   }
 
   type Version_ID = ID

 
   /** document structure **/
 
   /* 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
     Option[List[(Option[C], Option[C])]])  // None: remove, Some: insert/remove commands
 

     val init = new Change(Future.value(Version.init), Nil, Future.value(Nil, Version.init))
   }
 
   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)
     def is_finished: Boolean = previous.is_finished && version.is_finished
   }

         case Some(assgn) => assgn.is_finished
         case None => false
       }
 
     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)
       (change, copy(history = history + change))
     }

         change.is_finished && is_assigned(change.version.get_finished))
       require(found_stable.isDefined)
       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
       {
         val version = stable.version.get_finished