src/Pure/PIDE/document.scala

--- a/src/Pure/PIDE/document.scala	Fri Sep 02 16:58:00 2011 -0700
+++ b/src/Pure/PIDE/document.scala	Sat Sep 03 12:31:27 2011 +0200
@@ -168,15 +168,19 @@
 
   object Change
   {
-    val init: Change = Change(Future.value(Version.init), Nil, Future.value(Version.init))
+    val init: Change = Change(Some(Future.value(Version.init)), Nil, Future.value(Version.init))
   }
 
   sealed case class Change(
-    val previous: Future[Version],
+    val previous: Option[Future[Version]],
     val edits: List[Edit_Text],
     val version: Future[Version])
   {
-    def is_finished: Boolean = previous.is_finished && version.is_finished
+    def is_finished: Boolean =
+      (previous match { case None => true case Some(future) => future.is_finished }) &&
+      version.is_finished
+
+    def truncate: Change = copy(previous = None, edits = Nil)
   }
 
 
@@ -184,16 +188,16 @@
 
   object History
   {
-    val init: History = new History(List(Change.init))
+    val init: History = History(List(Change.init))
   }
 
   // FIXME pruning, purging of state
-  class History(val undo_list: List[Change])
+  sealed case class History(val undo_list: List[Change])
   {
     require(!undo_list.isEmpty)
 
     def tip: Change = undo_list.head
-    def +(change: Change): History = new History(change :: undo_list)
+    def +(change: Change): History = copy(undo_list = change :: undo_list)
   }
 
 
@@ -342,7 +346,7 @@
     def is_stable(change: Change): Boolean =
       change.is_finished && is_assigned(change.version.get_finished)
 
-    def recent_stable: Option[Change] = history.undo_list.find(is_stable)
+    def recent_stable: Change = history.undo_list.find(is_stable) getOrElse fail
     def tip_stable: Boolean = is_stable(history.tip)
     def tip_version: Version = history.tip.version.get_finished
 
@@ -366,10 +370,25 @@
         edits: List[Edit_Text],
         version: Future[Version]): (Change, State) =
     {
-      val change = Change(previous, edits, version)
+      val change = Change(Some(previous), edits, version)
       (change, copy(history = history + change))
     }
 
+    def prune_history(retain: Int = 0): (List[Version], State) =
+    {
+      val undo_list = history.undo_list
+      val n = undo_list.iterator.zipWithIndex.find(p => is_stable(p._1)).get._2 + 1
+      val (retained, dropped) = undo_list.splitAt(n max retain)
+
+      retained.splitAt(retained.length - 1) match {
+        case (prefix, List(last)) =>
+          val dropped_versions = dropped.map(change => change.version.get_finished)
+          val state1 = copy(history = History(prefix ::: List(last.truncate)))
+          (dropped_versions, state1)
+        case _ => fail
+      }
+    }
+
     def command_state(version: Version, command: Command): Command.State =
     {
       require(is_assigned(version))
@@ -384,7 +403,7 @@
     // persistent user-view
     def snapshot(name: Node.Name, pending_edits: List[Text.Edit]): Snapshot =
     {
-      val stable = recent_stable.get
+      val stable = recent_stable
       val latest = history.tip
 
       // FIXME proper treatment of removed nodes