src/Pure/PIDE/document.scala

--- a/src/Pure/PIDE/document.scala	Sat Aug 07 17:24:46 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Sat Aug 07 19:52:14 2010 +0200
@@ -14,33 +14,31 @@
 
 object Document
 {
-  /* unique identifiers */
+  /* formal identifiers */
 
+  type Version_ID = String
+  type Command_ID = String
   type State_ID = String
-  type Command_ID = String
-  type Version_ID = String
 
   val NO_ID = ""
 
 
-  /* command start positions */
 
-  def command_starts(commands: Iterator[Command], offset: Int = 0): Iterator[(Command, Int)] =
-  {
-    var i = offset
-    for (command <- commands) yield {
-      val start = i
-      i += command.length
-      (command, start)
-    }
-  }
-
-
-  /* named document nodes */
+  /** named document nodes **/
 
   object Node
   {
     val empty: Node = new Node(Linear_Set())
+
+    def command_starts(commands: Iterator[Command], offset: Int = 0): Iterator[(Command, Int)] =
+    {
+      var i = offset
+      for (command <- commands) yield {
+        val start = i
+        i += command.length
+        (command, start)
+      }
+    }
   }
 
   class Node(val commands: Linear_Set[Command])
@@ -48,7 +46,7 @@
     /* command ranges */
 
     def command_starts: Iterator[(Command, Int)] =
-      Document.command_starts(commands.iterator)
+      Node.command_starts(commands.iterator)
 
     def command_start(cmd: Command): Option[Int] =
       command_starts.find(_._1 == cmd).map(_._2)
@@ -85,7 +83,7 @@
 
 
 
-  /** editing **/
+  /** changes of plain text, eventually resulting in document edits **/
 
   type Node_Text_Edit = (String, List[Text_Edit])  // FIXME None: remove
 
@@ -93,6 +91,65 @@
    (String,  // node name
     Option[List[(Option[C], Option[C])]])  // None: remove, Some: insert/remove commands
 
+  abstract class Snapshot
+  {
+    val document: Document
+    val node: Document.Node
+    val is_outdated: Boolean
+    def convert(offset: Int): Int
+    def revert(offset: Int): Int
+  }
+
+  object Change
+  {
+    val init = new Change(NO_ID, None, Nil, Future.value(Nil, Document.init))
+  }
+
+  class Change(
+    val id: Version_ID,
+    val parent: Option[Change],
+    val edits: List[Node_Text_Edit],
+    val result: Future[(List[Edit[Command]], Document)])
+  {
+    def ancestors: Iterator[Change] = new Iterator[Change]
+    {
+      private var state: Option[Change] = Some(Change.this)
+      def hasNext = state.isDefined
+      def next =
+        state match {
+          case Some(change) => state = change.parent; change
+          case None => throw new NoSuchElementException("next on empty iterator")
+        }
+    }
+
+    def join_document: Document = result.join._2
+    def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished
+
+    def snapshot(name: String, pending_edits: List[Text_Edit]): Snapshot =
+    {
+      val latest = Change.this
+      val stable = latest.ancestors.find(_.is_assigned)
+      require(stable.isDefined)
+
+      val edits =
+        (pending_edits /: latest.ancestors.takeWhile(_ != stable.get))((edits, change) =>
+            (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
+      lazy val reverse_edits = edits.reverse
+
+      new Snapshot {
+        val document = stable.get.join_document
+        val node = document.nodes(name)
+        val is_outdated = !(pending_edits.isEmpty && latest == stable.get)
+        def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i))
+        def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i))
+      }
+    }
+  }
+
+
+
+  /** editing **/
+
   def text_edits(session: Session, old_doc: Document, new_id: Version_ID,
       edits: List[Node_Text_Edit]): (List[Edit[Command]], Document) =
   {
@@ -114,7 +171,7 @@
     {
       eds match {
         case e :: es =>
-          command_starts(commands.iterator).find {
+          Node.command_starts(commands.iterator).find {
             case (cmd, cmd_start) =>
               e.can_edit(cmd.source, cmd_start) ||
                 e.is_insert && e.start == cmd_start + cmd.length