some support to prune_history;
authorwenzelm
Sat Sep 03 12:31:27 2011 +0200 (2011-09-03)
changeset 4467207dad1433cd7
parent 44671 7f0b4515588a
child 44673 2fa51ac191bc
some support to prune_history;
clarified signature: recent_stable is supposed to be always defined;
src/Pure/PIDE/document.scala
src/Tools/jEdit/src/session_dockable.scala
     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
     2.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Fri Sep 02 16:58:00 2011 -0700
     2.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Sat Sep 03 12:31:27 2011 +0200
     2.3 @@ -80,23 +80,21 @@
     2.4      Swing_Thread.now {
     2.5        // FIXME correlation to changed_nodes!?
     2.6        val state = Isabelle.session.current_state()
     2.7 -      state.recent_stable.map(change => change.version.get_finished) match {
     2.8 -        case None =>
     2.9 -        case Some(version) =>
    2.10 -          var nodes_status1 = nodes_status
    2.11 -          for {
    2.12 -            name <- changed_nodes
    2.13 -            node <- version.nodes.get(name)
    2.14 -            val status = Isar_Document.node_status(state, version, node)
    2.15 -          } nodes_status1 += (name -> status.toString)
    2.16 +      val version = state.recent_stable.version.get_finished
    2.17  
    2.18 -          if (nodes_status != nodes_status1) {
    2.19 -            nodes_status = nodes_status1
    2.20 -            val order =
    2.21 -              Library.sort_wrt((name: Document.Node.Name) => name.theory,
    2.22 -                nodes_status.keySet.toList)
    2.23 -            status.listData = order.map(name => name.theory + " " + nodes_status(name))
    2.24 -          }
    2.25 +      var nodes_status1 = nodes_status
    2.26 +      for {
    2.27 +        name <- changed_nodes
    2.28 +        node <- version.nodes.get(name)
    2.29 +        val status = Isar_Document.node_status(state, version, node)
    2.30 +      } nodes_status1 += (name -> status.toString)
    2.31 +
    2.32 +      if (nodes_status != nodes_status1) {
    2.33 +        nodes_status = nodes_status1
    2.34 +        val order =
    2.35 +          Library.sort_wrt((name: Document.Node.Name) => name.theory,
    2.36 +            nodes_status.keySet.toList)
    2.37 +        status.listData = order.map(name => name.theory + " " + nodes_status(name))
    2.38        }
    2.39      }
    2.40    }