# HG changeset patch
# User wenzelm
# Date 1398416999 -7200
# Node ID 3438dfba58fe5269b5fe9478184e98a97a2a46ef
# Parent  c7cf653228ed598dadef471ff7ce9718e60a5b7e
more robust prover termination;

diff -r c7cf653228ed -r 3438dfba58fe src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Fri Apr 25 10:51:57 2014 +0200
+++ b/src/Pure/PIDE/session.scala	Fri Apr 25 11:09:59 2014 +0200
@@ -403,7 +403,7 @@
       def bad_output()
       {
         if (verbose)
-          System.err.println("Ignoring prover output: " + output.message.toString)
+          System.err.println("Ignoring bad prover output: " + output.message.toString)
       }
 
       def accumulate(state_id: Document_ID.Generic, message: XML.Elem)
@@ -475,6 +475,7 @@
               phase = Session.Ready
 
             case Markup.Return_Code(rc) if output.is_exit =>
+              prover = None
               if (rc == 0) phase = Session.Inactive
               else phase = Session.Failed
 
@@ -504,8 +505,6 @@
               global_state.change(_ => Document.State.init)  // FIXME event bus!?
               phase = Session.Shutdown
               prover.get.terminate
-              prover = None
-              phase = Session.Inactive
             }
 
           case Update_Options(options) =>