src/Pure/PIDE/document.scala
changeset 44672 07dad1433cd7
parent 44642 446fe2abe252
child 44676 7de87f1ae965
     1.1 --- a/src/Pure/PIDE/document.scala	Fri Sep 02 16:58:00 2011 -0700
     1.2 +++ b/src/Pure/PIDE/document.scala	Sat Sep 03 12:31:27 2011 +0200
     1.3 @@ -168,15 +168,19 @@
     1.4  
     1.5    object Change
     1.6    {
     1.7 -    val init: Change = Change(Future.value(Version.init), Nil, Future.value(Version.init))
     1.8 +    val init: Change = Change(Some(Future.value(Version.init)), Nil, Future.value(Version.init))
     1.9    }
    1.10  
    1.11    sealed case class Change(
    1.12 -    val previous: Future[Version],
    1.13 +    val previous: Option[Future[Version]],
    1.14      val edits: List[Edit_Text],
    1.15      val version: Future[Version])
    1.16    {
    1.17 -    def is_finished: Boolean = previous.is_finished && version.is_finished
    1.18 +    def is_finished: Boolean =
    1.19 +      (previous match { case None => true case Some(future) => future.is_finished }) &&
    1.20 +      version.is_finished
    1.21 +
    1.22 +    def truncate: Change = copy(previous = None, edits = Nil)
    1.23    }
    1.24  
    1.25  
    1.26 @@ -184,16 +188,16 @@
    1.27  
    1.28    object History
    1.29    {
    1.30 -    val init: History = new History(List(Change.init))
    1.31 +    val init: History = History(List(Change.init))
    1.32    }
    1.33  
    1.34    // FIXME pruning, purging of state
    1.35 -  class History(val undo_list: List[Change])
    1.36 +  sealed case class History(val undo_list: List[Change])
    1.37    {
    1.38      require(!undo_list.isEmpty)
    1.39  
    1.40      def tip: Change = undo_list.head
    1.41 -    def +(change: Change): History = new History(change :: undo_list)
    1.42 +    def +(change: Change): History = copy(undo_list = change :: undo_list)
    1.43    }
    1.44  
    1.45  
    1.46 @@ -342,7 +346,7 @@
    1.47      def is_stable(change: Change): Boolean =
    1.48        change.is_finished && is_assigned(change.version.get_finished)
    1.49  
    1.50 -    def recent_stable: Option[Change] = history.undo_list.find(is_stable)
    1.51 +    def recent_stable: Change = history.undo_list.find(is_stable) getOrElse fail
    1.52      def tip_stable: Boolean = is_stable(history.tip)
    1.53      def tip_version: Version = history.tip.version.get_finished
    1.54  
    1.55 @@ -366,10 +370,25 @@
    1.56          edits: List[Edit_Text],
    1.57          version: Future[Version]): (Change, State) =
    1.58      {
    1.59 -      val change = Change(previous, edits, version)
    1.60 +      val change = Change(Some(previous), edits, version)
    1.61        (change, copy(history = history + change))
    1.62      }
    1.63  
    1.64 +    def prune_history(retain: Int = 0): (List[Version], State) =
    1.65 +    {
    1.66 +      val undo_list = history.undo_list
    1.67 +      val n = undo_list.iterator.zipWithIndex.find(p => is_stable(p._1)).get._2 + 1
    1.68 +      val (retained, dropped) = undo_list.splitAt(n max retain)
    1.69 +
    1.70 +      retained.splitAt(retained.length - 1) match {
    1.71 +        case (prefix, List(last)) =>
    1.72 +          val dropped_versions = dropped.map(change => change.version.get_finished)
    1.73 +          val state1 = copy(history = History(prefix ::: List(last.truncate)))
    1.74 +          (dropped_versions, state1)
    1.75 +        case _ => fail
    1.76 +      }
    1.77 +    }
    1.78 +
    1.79      def command_state(version: Version, command: Command): Command.State =
    1.80      {
    1.81        require(is_assigned(version))
    1.82 @@ -384,7 +403,7 @@
    1.83      // persistent user-view
    1.84      def snapshot(name: Node.Name, pending_edits: List[Text.Edit]): Snapshot =
    1.85      {
    1.86 -      val stable = recent_stable.get
    1.87 +      val stable = recent_stable
    1.88        val latest = history.tip
    1.89  
    1.90        // FIXME proper treatment of removed nodes