postpone changes in intermediate state between remove_versions/removed_versions, which is important for handle_change to refer to defined items on prover side;

--- a/src/Pure/PIDE/document.scala	Fri Aug 15 13:39:59 2014 +0200
+++ b/src/Pure/PIDE/document.scala	Sun Aug 17 16:05:43 2014 +0200
@@ -499,7 +499,9 @@
     /*commands with markup produced by other commands (imm_succs)*/
     val commands_redirection: Graph[Document_ID.Command, Unit] = Graph.long,
     /*explicit (linear) history*/
-    val history: History = History.init)
+    val history: History = History.init,
+    /*intermediate state between remove_versions/removed_versions*/
+    val removing_versions: Boolean = false)
   {
     private def fail[A]: A = throw new State.Fail(this)
 
@@ -620,13 +622,14 @@
       copy(history = history + change)
     }
 
-    def prune_history(retain: Int = 0): (List[Version], State) =
+    def remove_versions(retain: Int = 0): (List[Version], State) =
     {
       history.prune(is_stable, retain) match {
         case Some((dropped, history1)) =>
-          val dropped_versions = dropped.map(change => change.version.get_finished)
-          val state1 = copy(history = history1)
-          (dropped_versions, state1)
+          val old_versions = dropped.map(change => change.version.get_finished)
+          val removing = !old_versions.isEmpty
+          val state1 = copy(history = history1, removing_versions = removing)
+          (old_versions, state1)
         case None => fail
       }
     }
@@ -661,7 +664,8 @@
         commands = commands1,
         execs = execs1,
         commands_redirection = commands_redirection.restrict(commands1.isDefinedAt(_)),
-        assignments = assignments1)
+        assignments = assignments1,
+        removing_versions = false)
     }
 
     private def command_states_self(version: Version, command: Command)

--- a/src/Pure/PIDE/session.scala	Fri Aug 15 13:39:59 2014 +0200
+++ b/src/Pure/PIDE/session.scala	Sun Aug 17 16:05:43 2014 +0200
@@ -52,6 +52,8 @@
     doc_edits: List[Document.Edit_Command],
     version: Document.Version)
 
+  case object Change_Flush
+
 
   /* events */
 
@@ -320,11 +322,10 @@
 
     def store(change: Session.Change): Unit = synchronized { postponed ::= change }
 
-    def flush(): Unit = synchronized {
-      val state = global_state.value
+    def flush(state: Document.State): List[Session.Change] = synchronized {
       val (assigned, unassigned) = postponed.partition(change => state.is_assigned(change.previous))
       postponed = unassigned
-      assigned.reverseIterator.foreach(change => manager.send(change))
+      assigned.reverse
     }
   }
 
@@ -448,9 +449,9 @@
                     try {
                       val cmds = global_state.change_result(_.assign(id, update))
                       change_buffer.invoke(true, cmds)
+                      manager.send(Session.Change_Flush)
                     }
                     catch { case _: Document.State.Fail => bad_output() }
-                    postponed_changes.flush()
                   case _ => bad_output()
                 }
                 delay_prune.invoke()
@@ -460,6 +461,7 @@
                   case Protocol.Removed(removed) =>
                     try {
                       global_state.change(_.removed_versions(removed))
+                      manager.send(Session.Change_Flush)
                     }
                     catch { case _: Document.State.Fail => bad_output() }
                   case _ => bad_output()
@@ -532,7 +534,7 @@
 
           case Prune_History =>
             if (prover.defined) {
-              val old_versions = global_state.change_result(_.prune_history(prune_size))
+              val old_versions = global_state.change_result(_.remove_versions(prune_size))
               if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
             }
 
@@ -557,10 +559,16 @@
             prover.get.protocol_command(name, args:_*)
 
           case change: Session.Change if prover.defined =>
-            if (global_state.value.is_assigned(change.previous))
+            val state = global_state.value
+            if (!state.removing_versions && state.is_assigned(change.previous))
               handle_change(change)
             else postponed_changes.store(change)
 
+          case Session.Change_Flush if prover.defined =>
+            val state = global_state.value
+            if (!state.removing_versions)
+              postponed_changes.flush(state).foreach(handle_change(_))
+
           case bad =>
             if (verbose) Output.warning("Ignoring bad message: " + bad.toString)
         }