src/Pure/PIDE/document.scala

 
   val NO_ID: ID = 0
 
 
 
-  /** named document nodes **/
+  /** document structure **/
+
+  /* named nodes -- development graph */
+
+  type Node_Text_Edit = (String, List[Text_Edit])  // FIXME None: remove
+
+  type Edit[C] =
+   (String,  // node name
+    Option[List[(Option[C], Option[C])]])  // None: remove, Some: insert/remove commands
 
   object Node
   {
     val empty: Node = new Node(Linear_Set())
 
+    // FIXME not scalable
     def command_starts(commands: Iterator[Command], offset: Int = 0): Iterator[(Command, Int)] =
     {
       var i = offset
       for (command <- commands) yield {
         val start = i

     }
   }
 
   class Node(val commands: Linear_Set[Command])
   {
-    /* command ranges */
-
     def command_starts: Iterator[(Command, Int)] =
       Node.command_starts(commands.iterator)
 
     def command_start(cmd: Command): Option[Int] =
       command_starts.find(_._1 == cmd).map(_._2)

         case None => None
       }
   }
 
 
-  /* document versions */
+
+  /** versioning **/
+
+  /* particular document versions */
 
   object Version
   {
     val init: Version = new Version(NO_ID, Map().withDefaultValue(Node.empty))
   }
 
   class Version(val id: Version_ID, val nodes: Map[String, Node])
 
 
-
-  /** changes of plain text, eventually resulting in document edits **/
-
-  type Node_Text_Edit = (String, List[Text_Edit])  // FIXME None: remove
-
-  type Edit[C] =
-   (String,  // node name
-    Option[List[(Option[C], Option[C])]])  // None: remove, Some: insert/remove commands
+  /* changes of plain text, eventually resulting in document edits */
+
+  object Change
+  {
+    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 result: Future[(List[Edit[Command]], Version)])
+  {
+    val current: Future[Version] = result.map(_._2)
+    def is_finished: Boolean = previous.is_finished && current.is_finished
+  }
+
+
+  /* history navigation and persistent snapshots */
 
   abstract class Snapshot
   {
     val version: Version
     val node: Node

     def revert(offset: Int): Int
     def lookup_command(id: Command_ID): Option[Command]
     def state(command: Command): Command.State
   }
 
-  object Change
-  {
-    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 result: Future[(List[Edit[Command]], Version)])
-  {
-    val current: Future[Version] = result.map(_._2)
-    def is_finished: Boolean = previous.is_finished && current.is_finished
+  object History
+  {
+    val init = new History(List(Change.init))
+  }
+
+  // FIXME pruning, purging of state
+  class History(undo_list: List[Change])
+  {
+    require(!undo_list.isEmpty)
+
+    def tip: Change = undo_list.head
+    def +(ch: Change): History = new History(ch :: undo_list)
+
+    def snapshot(name: String, pending_edits: List[Text_Edit], state_snapshot: State): Snapshot =
+    {
+      val found_stable = undo_list.find(change =>
+        change.is_finished && state_snapshot.is_assigned(change.current.join))
+      require(found_stable.isDefined)
+      val stable = found_stable.get
+      val latest = undo_list.head
+
+      val edits =
+        (pending_edits /: undo_list.takeWhile(_ != stable))((edits, change) =>
+            (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
+      lazy val reverse_edits = edits.reverse
+
+      new Snapshot
+      {
+        val version = stable.current.join
+        val node = version.nodes(name)
+        val is_outdated = !(pending_edits.isEmpty && latest == stable)
+        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))
+        def lookup_command(id: Command_ID): Option[Command] = state_snapshot.lookup_command(id)
+        def state(command: Command): Command.State =
+          try { state_snapshot.command_state(version, command) }
+          catch { case _: State.Fail => command.empty_state }
+      }
+    }
   }
 
 
 
   /** global state -- document structure and execution process **/