--- 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