clarified signature: explicit exit_state;

--- a/src/Pure/Build/build_job.scala	Sat Oct 18 17:29:39 2025 +0200
+++ b/src/Pure/Build/build_job.scala	Sat Oct 18 18:25:16 2025 +0200
@@ -338,7 +338,7 @@
           }
 
           session.init_protocol_handler(new Session.Protocol_Handler {
-              override def exit(): Unit = session.errors_cancel()
+              override def exit(exit_state: Document.State): Unit = session.errors_cancel()
 
               private def build_session_finished(msg: Prover.Protocol_Output): Boolean = {
                 val (rc, errors) =

--- a/src/Pure/ML/ml_statistics.scala	Sat Oct 18 17:29:39 2025 +0200
+++ b/src/Pure/ML/ml_statistics.scala	Sat Oct 18 18:25:16 2025 +0200
@@ -78,7 +78,7 @@
       this.session = session
     }
 
-    override def exit(): Unit = synchronized {
+    override def exit(exit_state: Document.State): Unit = synchronized {
       session = null
       monitoring.cancel()
     }

--- a/src/Pure/PIDE/protocol_handlers.scala	Sat Oct 18 17:29:39 2025 +0200
+++ b/src/Pure/PIDE/protocol_handlers.scala	Sat Oct 18 18:25:16 2025 +0200
@@ -55,8 +55,8 @@
         case _ => false
       }
 
-    def exit(): State = {
-      for ((_, handler) <- handlers) handler.exit()
+    def exit(exit_state: Document.State): State = {
+      for ((_, handler) <- handlers) handler.exit(exit_state)
       copy(handlers = Map.empty, functions = Map.empty)
     }
   }
@@ -77,5 +77,5 @@
   def init(handler: Session.Protocol_Handler): Unit = state.change(_.init(handler))
   def init(name: String): Unit = state.change(_.init(name))
   def invoke(msg: Prover.Protocol_Output): Boolean = state.value.invoke(msg)
-  def exit(): Unit = state.change(_.exit())
+  def exit(exit_state: Document.State): Unit = state.change(_.exit(exit_state))
 }

--- a/src/Pure/PIDE/session.scala	Sat Oct 18 17:29:39 2025 +0200
+++ b/src/Pure/PIDE/session.scala	Sat Oct 18 18:25:16 2025 +0200
@@ -116,7 +116,7 @@
 
   abstract class Protocol_Handler extends Isabelle_System.Service {
     def init(session: Session): Unit = {}
-    def exit(): Unit = {}
+    def exit(state: Document.State): Unit = {}
     def functions: Protocol_Functions = Nil
     def prover_options(options: Options): Options = options
   }
@@ -618,8 +618,9 @@
               }
 
             case Markup.Process_Result(result) if output.is_exit =>
-              if (prover.defined) protocol_handlers.exit()
-              for (id <- global_state.value.theories.keys) {
+              val exit_state = global_state.value
+              if (prover.defined) protocol_handlers.exit(exit_state)
+              for (id <- exit_state.theories.keys) {
                 val snapshot = global_state.change_result(_.end_theory(id, build_blobs))
                 finished_theories.post(snapshot)
               }

--- a/src/Pure/System/bash.scala	Sat Oct 18 17:29:39 2025 +0200
+++ b/src/Pure/System/bash.scala	Sat Oct 18 18:25:16 2025 +0200
@@ -428,12 +428,13 @@
       server = Server.start(debugging = session.session_options.bool("bash_process_debugging"))
     }
 
-    override def exit(): Unit = {
+    def exit(): Unit =
       if (server != null) {
         server.stop()
         server = null
       }
-    }
+
+    override def exit(exit_state: Document.State): Unit = exit()
 
     override def prover_options(options: Options): Options = {
       val address = if (server == null) "" else server.address

--- a/src/Pure/System/scala.scala	Sat Oct 18 17:29:39 2025 +0200
+++ b/src/Pure/System/scala.scala	Sat Oct 18 18:25:16 2025 +0200
@@ -296,7 +296,7 @@
     override def init(session: Session): Unit =
       synchronized { this.session = session }
 
-    override def exit(): Unit = synchronized {
+    override def exit(exit_state: Document.State): Unit = synchronized {
       for ((id, future) <- futures) cancel(id, future)
       futures = Map.empty
     }

--- a/src/Pure/Tools/simplifier_trace.scala	Sat Oct 18 17:29:39 2025 +0200
+++ b/src/Pure/Tools/simplifier_trace.scala	Sat Oct 18 18:25:16 2025 +0200
@@ -293,7 +293,7 @@
       the_session = session
     }
 
-    override def exit(): Unit = {
+    override def exit(exit_state: Document.State): Unit = {
       val session = the_session
       if (session != null) {
         val manager = the_manager(session)