src/Pure/PIDE/document.scala

 
   /* changes of plain text, eventually resulting in document edits */
 
   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)
   }
 
 
   /* history navigation */
 
   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)
   }
 
 
 
   /** global state -- document structure, execution process, editing history **/

       }
 
     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
 
     def last_exec_offset(name: Node.Name): Text.Offset =
     {

     def continue_history(
         previous: Future[Version],
         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))

 
 
     // 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
       val edits =
         (pending_edits /: history.undo_list.takeWhile(_ != stable))((edits, change) =>