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)

     2.1 --- a/src/Pure/PIDE/session.scala	Fri Aug 15 13:39:59 2014 +0200
     2.2 +++ b/src/Pure/PIDE/session.scala	Sun Aug 17 16:05:43 2014 +0200
     2.3 @@ -52,6 +52,8 @@
     2.4      doc_edits: List[Document.Edit_Command],
     2.5      version: Document.Version)
     2.6  
     2.7 +  case object Change_Flush
     2.8 +
     2.9  
    2.10    /* events */
    2.11  
    2.12 @@ -320,11 +322,10 @@
    2.13  
    2.14      def store(change: Session.Change): Unit = synchronized { postponed ::= change }
    2.15  
    2.16 -    def flush(): Unit = synchronized {
    2.17 -      val state = global_state.value
    2.18 +    def flush(state: Document.State): List[Session.Change] = synchronized {
    2.19        val (assigned, unassigned) = postponed.partition(change => state.is_assigned(change.previous))
    2.20        postponed = unassigned
    2.21 -      assigned.reverseIterator.foreach(change => manager.send(change))
    2.22 +      assigned.reverse
    2.23      }
    2.24    }
    2.25  
    2.26 @@ -448,9 +449,9 @@
    2.27                      try {
    2.28                        val cmds = global_state.change_result(_.assign(id, update))
    2.29                        change_buffer.invoke(true, cmds)
    2.30 +                      manager.send(Session.Change_Flush)
    2.31                      }
    2.32                      catch { case _: Document.State.Fail => bad_output() }
    2.33 -                    postponed_changes.flush()
    2.34                    case _ => bad_output()
    2.35                  }
    2.36                  delay_prune.invoke()
    2.37 @@ -460,6 +461,7 @@
    2.38                    case Protocol.Removed(removed) =>
    2.39                      try {
    2.40                        global_state.change(_.removed_versions(removed))
    2.41 +                      manager.send(Session.Change_Flush)
    2.42                      }
    2.43                      catch { case _: Document.State.Fail => bad_output() }
    2.44                    case _ => bad_output()
    2.45 @@ -532,7 +534,7 @@
    2.46  
    2.47            case Prune_History =>
    2.48              if (prover.defined) {
    2.49 -              val old_versions = global_state.change_result(_.prune_history(prune_size))
    2.50 +              val old_versions = global_state.change_result(_.remove_versions(prune_size))
    2.51                if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
    2.52              }
    2.53  
    2.54 @@ -557,10 +559,16 @@
    2.55              prover.get.protocol_command(name, args:_*)
    2.56  
    2.57            case change: Session.Change if prover.defined =>
    2.58 -            if (global_state.value.is_assigned(change.previous))
    2.59 +            val state = global_state.value
    2.60 +            if (!state.removing_versions && state.is_assigned(change.previous))
    2.61                handle_change(change)
    2.62              else postponed_changes.store(change)
    2.63  
    2.64 +          case Session.Change_Flush if prover.defined =>
    2.65 +            val state = global_state.value
    2.66 +            if (!state.removing_versions)
    2.67 +              postponed_changes.flush(state).foreach(handle_change(_))
    2.68 +
    2.69            case bad =>
    2.70              if (verbose) Output.warning("Ignoring bad message: " + bad.toString)
    2.71          }