unified type Document.Edit;

--- a/src/Pure/PIDE/document.scala	Thu Nov 11 16:48:46 2010 +0100
+++ b/src/Pure/PIDE/document.scala	Thu Nov 11 17:07:05 2010 +0100
@@ -35,13 +35,13 @@
 
   /* named nodes -- development graph */
 
-  type Text_Edit =
+  type Edit[A] =
    (String,  // node name
-    Option[List[Text.Edit]])  // None: remove, Some: insert/remove text
+    Option[List[A]])  // None: remove node, Some: edit content
 
-  type Edit[C] =
-   (String,  // node name
-    Option[List[(Option[C], Option[C])]])  // None: remove, Some: insert/remove commands
+  type Edit_Text = Edit[Text.Edit]
+  type Edit_Command = Edit[(Option[Command], Option[Command])]
+  type Edit_Command_ID = Edit[(Option[Command_ID], Option[Command_ID])]
 
   object Node
   {
@@ -136,8 +136,8 @@
 
   class Change(
     val previous: Future[Version],
-    val edits: List[Text_Edit],
-    val result: Future[(List[Edit[Command]], Version)])
+    val edits: List[Edit_Text],
+    val result: Future[(List[Edit_Command], Version)])
   {
     val version: Future[Version] = result.map(_._2)
     def is_finished: Boolean = previous.is_finished && version.is_finished
@@ -270,8 +270,8 @@
       }
 
     def extend_history(previous: Future[Version],
-        edits: List[Text_Edit],
-        result: Future[(List[Edit[Command]], Version)]): (Change, State) =
+        edits: List[Edit_Text],
+        result: Future[(List[Edit_Command], Version)]): (Change, State) =
     {
       val change = new Change(previous, edits, result)
       (change, copy(history = history + change))

--- a/src/Pure/PIDE/isar_document.scala	Thu Nov 11 16:48:46 2010 +0100
+++ b/src/Pure/PIDE/isar_document.scala	Thu Nov 11 17:07:05 2010 +0100
@@ -140,7 +140,7 @@
   /* document versions */
 
   def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
-      edits: List[Document.Edit[Document.Command_ID]])
+      edits: List[Document.Edit_Command_ID])
   {
     val arg =
       XML_Data.make_list(

--- a/src/Pure/System/session.scala	Thu Nov 11 16:48:46 2010 +0100
+++ b/src/Pure/System/session.scala	Thu Nov 11 17:07:05 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.Text_Edit])
+  private case class Edit_Version(edits: List[Document.Edit_Text])
   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.Text_Edit]) { session_actor !? Edit_Version(edits) }
+  def edit_version(edits: List[Document.Edit_Text]) { session_actor !? Edit_Version(edits) }
 
   def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
     global_state.peek().snapshot(name, pending_edits)

--- a/src/Pure/Thy/thy_syntax.scala	Thu Nov 11 16:48:46 2010 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Thu Nov 11 17:07:05 2010 +0100
@@ -100,7 +100,7 @@
   /** text edits **/
 
   def text_edits(session: Session, previous: Document.Version,
-      edits: List[Document.Text_Edit]): (List[Document.Edit[Command]], Document.Version) =
+      edits: List[Document.Edit_Text]): (List[Document.Edit_Command], Document.Version) =
   {
     /* phase 1: edit individual command source */
 
@@ -172,7 +172,7 @@
     /* resulting document edits */
 
     {
-      val doc_edits = new mutable.ListBuffer[Document.Edit[Command]]
+      val doc_edits = new mutable.ListBuffer[Document.Edit_Command]
       var nodes = previous.nodes
 
       edits foreach {