src/Pure/PIDE/session.scala

     /* raw edits */
 
     def handle_raw_edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
     //{{{
     {
+      require(prover.isDefined)
+
       prover.get.discontinue_execution()
 
       val previous = global_state.value.history.tip.version
       val version = Future.promise[Document.Version]
       global_state.change(_.continue_history(previous, edits, version))

     /* resulting changes */
 
     def handle_change(change: Session.Change)
     //{{{
     {
+      require(prover.isDefined)
+
       def id_command(command: Command)
       {
         for {
           digest <- command.blobs_digests
           if !global_state.value.defined_blob(digest)

       output match {
         case msg: Prover.Protocol_Output =>
           val handled = _protocol_handlers.invoke(msg)
           if (!handled) {
             msg.properties match {
-              case Markup.Protocol_Handler(name) =>
+              case Markup.Protocol_Handler(name) if prover.isDefined =>
                 _protocol_handlers = _protocol_handlers.add(prover.get, name)
 
-              case Protocol.Command_Timing(state_id, timing) =>
+              case Protocol.Command_Timing(state_id, timing) if prover.isDefined =>
                 val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
                 accumulate(state_id, prover.get.xml_cache.elem(message))
 
               case Markup.Assign_Update =>
                 msg.text match {

               phase = Session.Startup
               prover = Some(resources.start_prover(receiver.invoke _, name, args))
             }
 
           case Stop =>
-            if (phase == Session.Ready) {
+            if (prover.isDefined && is_ready) {
               _protocol_handlers = _protocol_handlers.stop(prover.get)
               global_state.change(_ => Document.State.init)  // FIXME event bus!?
               phase = Session.Shutdown
               prover.get.terminate
               prover = None