# HG changeset patch
# User wenzelm
# Date 1310224448 -7200
# Node ID c3ddb5537a2f20afc75ef8e67503815184e07371
# Parent  1d64662c1bfdad44423669eef6d08845c5fb70d7
more precise treatment of prover definedness;

diff -r 1d64662c1bfd -r c3ddb5537a2f src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Sat Jul 09 16:53:19 2011 +0200
+++ b/src/Pure/System/session.scala	Sat Jul 09 17:14:08 2011 +0200
@@ -303,13 +303,14 @@
             global_state.change(_ => Document.State.init)  // FIXME event bus!?
             phase = Session.Shutdown
             prover.get.terminate
+            prover = None
             phase = Session.Inactive
           }
           finished = true
           reply(())
 
-        case Interrupt =>
-          prover.map(_.interrupt)
+        case Interrupt if prover.isDefined =>
+          prover.get.interrupt
 
         case Edit_Node(name, header, text_edits) if prover.isDefined =>
           val node_name = (header.master_dir + Path.basic(name)).implode  // FIXME
@@ -331,8 +332,7 @@
         case result: Isabelle_Process.Result =>
           handle_result(result)
 
-        case bad if prover.isDefined =>
-          System.err.println("session_actor: ignoring bad message " + bad)
+        case bad => System.err.println("session_actor: ignoring bad message " + bad)
       }
     }
     //}}}