more robust prover termination;
authorwenzelm
Fri, 25 Apr 2014 11:09:59 +0200
changeset 56713 3438dfba58fe
parent 56712 c7cf653228ed
child 56714 061f83259922
more robust prover termination;
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) =>