more thorough protocol_handlers.exit, like file_formats.stop_session;
authorwenzelm
Fri, 07 Aug 2020 21:21:44 +0200
changeset 72115 c998827f1df9
parent 72114 d00220799735
child 72116 7773ec172572
more thorough protocol_handlers.exit, like file_formats.stop_session;
src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Fri Aug 07 21:02:02 2020 +0200
+++ b/src/Pure/PIDE/session.scala	Fri Aug 07 21:21:44 2020 +0200
@@ -555,6 +555,7 @@
               debugger.ready()
 
             case Markup.Process_Result(result) if output.is_exit =>
+              if (prover.defined) protocol_handlers.exit()
               file_formats.stop_session
               phase = Session.Terminated(result)
               prover.reset
@@ -596,7 +597,6 @@
             consolidation.exit()
             delay_prune.revoke()
             if (prover.defined) {
-              protocol_handlers.exit()
               global_state.change(_ => Document.State.init)
               prover.get.terminate
             }