src/Pure/PIDE/protocol_handlers.scala

--- 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))
 }