src/Pure/PIDE/session.scala

 
   /* protocol handlers */
 
   abstract class Protocol_Handler
   {
-    def start(prover: Prover): Unit = {}
+    def start(session: Session, prover: Prover): Unit = {}
     def stop(prover: Prover): Unit = {}
     val functions: Map[String, (Prover, Prover.Protocol_Output) => Boolean]
   }
 
   def bad_protocol_handler(exn: Throwable, name: String): Unit =

     handlers: Map[String, Session.Protocol_Handler] = Map.empty,
     functions: Map[String, Prover.Protocol_Output => Boolean] = Map.empty)
   {
     def get(name: String): Option[Protocol_Handler] = handlers.get(name)
 
-    def add(prover: Prover, handler: Protocol_Handler): Protocol_Handlers =
+    def add(session: Session, prover: Prover, handler: Protocol_Handler): Protocol_Handlers =
     {
       val name = handler.getClass.getName
 
       val (handlers1, functions1) =
         handlers.get(name) match {

           case None => (handlers, functions)
         }
 
       val (handlers2, functions2) =
         try {
-          handler.start(prover)
+          handler.start(session, prover)
 
           val new_functions =
             for ((a, f) <- handler.functions.toList) yield
               (a, (msg: Prover.Protocol_Output) => f(prover, msg))
 

 
   def get_protocol_handler(name: String): Option[Session.Protocol_Handler] =
     _protocol_handlers.value.get(name)
 
   def add_protocol_handler(handler: Session.Protocol_Handler): Unit =
-    _protocol_handlers.change(_.add(prover.get, handler))
+    _protocol_handlers.change(_.add(this, prover.get, handler))
 
 
   /* manager thread */
 
   private val delay_prune =