src/Pure/PIDE/document.scala
changeset 57976 bf99106b6672
parent 57842 8e4ae2db1849
child 59077 7e0d3da6e6d8
     1.1 --- a/src/Pure/PIDE/document.scala	Fri Aug 15 13:39:59 2014 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Sun Aug 17 16:05:43 2014 +0200
     1.3 @@ -499,7 +499,9 @@
     1.4      /*commands with markup produced by other commands (imm_succs)*/
     1.5      val commands_redirection: Graph[Document_ID.Command, Unit] = Graph.long,
     1.6      /*explicit (linear) history*/
     1.7 -    val history: History = History.init)
     1.8 +    val history: History = History.init,
     1.9 +    /*intermediate state between remove_versions/removed_versions*/
    1.10 +    val removing_versions: Boolean = false)
    1.11    {
    1.12      private def fail[A]: A = throw new State.Fail(this)
    1.13  
    1.14 @@ -620,13 +622,14 @@
    1.15        copy(history = history + change)
    1.16      }
    1.17  
    1.18 -    def prune_history(retain: Int = 0): (List[Version], State) =
    1.19 +    def remove_versions(retain: Int = 0): (List[Version], State) =
    1.20      {
    1.21        history.prune(is_stable, retain) match {
    1.22          case Some((dropped, history1)) =>
    1.23 -          val dropped_versions = dropped.map(change => change.version.get_finished)
    1.24 -          val state1 = copy(history = history1)
    1.25 -          (dropped_versions, state1)
    1.26 +          val old_versions = dropped.map(change => change.version.get_finished)
    1.27 +          val removing = !old_versions.isEmpty
    1.28 +          val state1 = copy(history = history1, removing_versions = removing)
    1.29 +          (old_versions, state1)
    1.30          case None => fail
    1.31        }
    1.32      }
    1.33 @@ -661,7 +664,8 @@
    1.34          commands = commands1,
    1.35          execs = execs1,
    1.36          commands_redirection = commands_redirection.restrict(commands1.isDefinedAt(_)),
    1.37 -        assignments = assignments1)
    1.38 +        assignments = assignments1,
    1.39 +        removing_versions = false)
    1.40      }
    1.41  
    1.42      private def command_states_self(version: Version, command: Command)