# HG changeset patch
# User wenzelm
# Date 1489498990 -3600
# Node ID b11099b7d868c601c7be15c91d5f8a8079696ac5
# Parent  912c3b9f77eea407c8dcef19504c59206e5a6c4c
clarified shutdown;

diff -r 912c3b9f77ee -r b11099b7d868 src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Tue Mar 14 13:27:39 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala	Tue Mar 14 14:43:10 2017 +0100
@@ -246,7 +246,7 @@
             reply("")
           case Session.Terminated(rc) if rc != 0 =>
             session.phase_changed -= session_phase
-            reply("Prover startup failed")
+            reply("Prover startup failed: return code " + rc)
           case _ =>
         }
       session.phase_changed += session_phase
@@ -262,22 +262,21 @@
 
     session_.change({
       case Some(session) =>
+        session.commands_changed -= prover_output
+        session.all_messages -= syslog
+
         dynamic_output.exit()
-        var session_phase: Session.Consumer[Session.Phase] = null
-        session_phase =
-          Session.Consumer(getClass.getName) {
-            case Session.Terminated(_) =>
-              session.phase_changed -= session_phase
-              session.commands_changed -= prover_output
-              session.all_messages -= syslog
-              reply("")
-            case _ =>
-          }
-        session.phase_changed += session_phase
-        session.stop()
+
+        delay_load.revoke()
+        file_watcher.shutdown()
         delay_input.revoke()
         delay_output.revoke()
-        file_watcher.shutdown()
+        delay_caret_update.revoke()
+
+        val rc = session.stop()
+        if (rc == 0) reply("")
+        else reply("Prover shutdown failed: return code " + rc)
+
         None
       case None =>
         reply("Prover inactive")