moved History/Snapshot to document.scala;

--- a/src/Pure/PIDE/document.scala	Sun Aug 15 20:27:29 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Sun Aug 15 21:03:13 2010 +0200
@@ -30,12 +30,21 @@
 
 
 
-  /** 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
@@ -49,8 +58,6 @@
 
   class Node(val commands: Linear_Set[Command])
   {
-    /* command ranges */
-
     def command_starts: Iterator[(Command, Int)] =
       Node.command_starts(commands.iterator)
 
@@ -78,7 +85,10 @@
   }
 
 
-  /* document versions */
+
+  /** versioning **/
+
+  /* particular document versions */
 
   object Version
   {
@@ -88,25 +98,7 @@
   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
-
-  abstract class Snapshot
-  {
-    val version: Version
-    val node: Node
-    val is_outdated: Boolean
-    def convert(offset: Int): Int
-    def revert(offset: Int): Int
-    def lookup_command(id: Command_ID): Option[Command]
-    def state(command: Command): Command.State
-  }
+  /* changes of plain text, eventually resulting in document edits */
 
   object Change
   {
@@ -123,6 +115,61 @@
   }
 
 
+  /* history navigation and persistent snapshots */
+
+  abstract class Snapshot
+  {
+    val version: Version
+    val node: Node
+    val is_outdated: Boolean
+    def convert(offset: Int): Int
+    def revert(offset: Int): Int
+    def lookup_command(id: Command_ID): Option[Command]
+    def state(command: Command): Command.State
+  }
+
+  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 **/
 

--- a/src/Pure/System/session.scala	Sun Aug 15 20:27:29 2010 +0200
+++ b/src/Pure/System/session.scala	Sun Aug 15 21:03:13 2010 +0200
@@ -290,56 +290,26 @@
 
   private val editor_history = new Actor
   {
-    @volatile private var history = List(Document.Change.init)
+    @volatile private var history = Document.History.init
 
     def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot =
-    {
-      val state_snapshot = current_state()
-      val history_snapshot = history
-
-      val found_stable = history_snapshot.find(change =>
-        change.is_finished && state_snapshot.is_assigned(change.current.join))
-      require(found_stable.isDefined)
-      val stable = found_stable.get
-      val latest = history_snapshot.head
-
-      val edits =
-        (pending_edits /: history_snapshot.takeWhile(_ != stable))((edits, change) =>
-            (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
-      lazy val reverse_edits = edits.reverse
-
-      new Document.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: Document.Command_ID): Option[Command] =
-          state_snapshot.lookup_command(id)
-        def state(command: Command): Command.State =
-          try { state_snapshot.command_state(version, command) }
-          catch { case _: Document.State.Fail => command.empty_state }
-      }
-    }
+      history.snapshot(name, pending_edits, current_state())
 
     def act
     {
       loop {
         react {
           case Edit_Version(edits) =>
-            val history_snapshot = history
-            require(!history_snapshot.isEmpty)
-
-            val prev = history_snapshot.head.current
+            val prev = history.tip.current
             val result =
               isabelle.Future.fork {
                 val previous = prev.join
                 val former_assignment = current_state().the_assignment(previous).join  // FIXME async!?
                 Thy_Syntax.text_edits(Session.this, previous, edits)
               }
-            val new_change = new Document.Change(prev, edits, result)
-            history ::= new_change
-            new_change.current.map(_ => session_actor ! new_change)
+            val change = new Document.Change(prev, edits, result)
+            history += change
+            change.current.map(_ => session_actor ! change)
             reply(())
 
           case bad => System.err.println("editor_model: ignoring bad message " + bad)