src/Pure/PIDE/session.scala
changeset 57979 fc136831d6ca
parent 57923 cdae2467311d
parent 57976 bf99106b6672
child 58928 23d0ffd48006
     1.1 --- a/src/Pure/PIDE/session.scala	Sun Aug 17 22:27:58 2014 +0200
     1.2 +++ b/src/Pure/PIDE/session.scala	Mon Aug 18 13:19:04 2014 +0200
     1.3 @@ -52,6 +52,8 @@
     1.4      doc_edits: List[Document.Edit_Command],
     1.5      version: Document.Version)
     1.6  
     1.7 +  case object Change_Flush
     1.8 +
     1.9  
    1.10    /* events */
    1.11  
    1.12 @@ -320,11 +322,10 @@
    1.13  
    1.14      def store(change: Session.Change): Unit = synchronized { postponed ::= change }
    1.15  
    1.16 -    def flush(): Unit = synchronized {
    1.17 -      val state = global_state.value
    1.18 +    def flush(state: Document.State): List[Session.Change] = synchronized {
    1.19        val (assigned, unassigned) = postponed.partition(change => state.is_assigned(change.previous))
    1.20        postponed = unassigned
    1.21 -      assigned.reverseIterator.foreach(change => manager.send(change))
    1.22 +      assigned.reverse
    1.23      }
    1.24    }
    1.25  
    1.26 @@ -448,9 +449,9 @@
    1.27                      try {
    1.28                        val cmds = global_state.change_result(_.assign(id, update))
    1.29                        change_buffer.invoke(true, cmds)
    1.30 +                      manager.send(Session.Change_Flush)
    1.31                      }
    1.32                      catch { case _: Document.State.Fail => bad_output() }
    1.33 -                    postponed_changes.flush()
    1.34                    case _ => bad_output()
    1.35                  }
    1.36                  delay_prune.invoke()
    1.37 @@ -460,6 +461,7 @@
    1.38                    case Protocol.Removed(removed) =>
    1.39                      try {
    1.40                        global_state.change(_.removed_versions(removed))
    1.41 +                      manager.send(Session.Change_Flush)
    1.42                      }
    1.43                      catch { case _: Document.State.Fail => bad_output() }
    1.44                    case _ => bad_output()
    1.45 @@ -532,7 +534,7 @@
    1.46  
    1.47            case Prune_History =>
    1.48              if (prover.defined) {
    1.49 -              val old_versions = global_state.change_result(_.prune_history(prune_size))
    1.50 +              val old_versions = global_state.change_result(_.remove_versions(prune_size))
    1.51                if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
    1.52              }
    1.53  
    1.54 @@ -557,10 +559,16 @@
    1.55              prover.get.protocol_command(name, args:_*)
    1.56  
    1.57            case change: Session.Change if prover.defined =>
    1.58 -            if (global_state.value.is_assigned(change.previous))
    1.59 +            val state = global_state.value
    1.60 +            if (!state.removing_versions && state.is_assigned(change.previous))
    1.61                handle_change(change)
    1.62              else postponed_changes.store(change)
    1.63  
    1.64 +          case Session.Change_Flush if prover.defined =>
    1.65 +            val state = global_state.value
    1.66 +            if (!state.removing_versions)
    1.67 +              postponed_changes.flush(state).foreach(handle_change(_))
    1.68 +
    1.69            case bad =>
    1.70              if (verbose) Output.warning("Ignoring bad message: " + bad.toString)
    1.71          }