more explicit checks;
authorwenzelm
Fri Apr 25 10:51:57 2014 +0200 (2014-04-25)
changeset 56712c7cf653228ed
parent 56711 ef3d00153e3b
child 56713 3438dfba58fe
more explicit checks;
src/Pure/PIDE/session.scala
     1.1 --- a/src/Pure/PIDE/session.scala	Thu Apr 24 23:21:00 2014 +0200
     1.2 +++ b/src/Pure/PIDE/session.scala	Fri Apr 25 10:51:57 2014 +0200
     1.3 @@ -341,6 +341,8 @@
     1.4      def handle_raw_edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
     1.5      //{{{
     1.6      {
     1.7 +      require(prover.isDefined)
     1.8 +
     1.9        prover.get.discontinue_execution()
    1.10  
    1.11        val previous = global_state.value.history.tip.version
    1.12 @@ -358,6 +360,8 @@
    1.13      def handle_change(change: Session.Change)
    1.14      //{{{
    1.15      {
    1.16 +      require(prover.isDefined)
    1.17 +
    1.18        def id_command(command: Command)
    1.19        {
    1.20          for {
    1.21 @@ -418,10 +422,10 @@
    1.22            val handled = _protocol_handlers.invoke(msg)
    1.23            if (!handled) {
    1.24              msg.properties match {
    1.25 -              case Markup.Protocol_Handler(name) =>
    1.26 +              case Markup.Protocol_Handler(name) if prover.isDefined =>
    1.27                  _protocol_handlers = _protocol_handlers.add(prover.get, name)
    1.28  
    1.29 -              case Protocol.Command_Timing(state_id, timing) =>
    1.30 +              case Protocol.Command_Timing(state_id, timing) if prover.isDefined =>
    1.31                  val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
    1.32                  accumulate(state_id, prover.get.xml_cache.elem(message))
    1.33  
    1.34 @@ -495,7 +499,7 @@
    1.35              }
    1.36  
    1.37            case Stop =>
    1.38 -            if (phase == Session.Ready) {
    1.39 +            if (prover.isDefined && is_ready) {
    1.40                _protocol_handlers = _protocol_handlers.stop(prover.get)
    1.41                global_state.change(_ => Document.State.init)  // FIXME event bus!?
    1.42                phase = Session.Shutdown