src/Pure/PIDE/session.scala

     def start(prover: Prover): Unit = {}
     def stop(prover: Prover): Unit = {}
     val functions: Map[String, (Prover, Prover.Protocol_Output) => Boolean]
   }
 
-  class Protocol_Handlers(
+  private class Protocol_Handlers(
     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 recent_syntax(name: Document.Node.Name): Prover.Syntax =
     current_state().recent_finished.version.get_finished.nodes(name).syntax getOrElse
     resources.base_syntax
 
 
-  /* protocol handlers */
-
-  @volatile private var _protocol_handlers = new Session.Protocol_Handlers()
-
-  def protocol_handler(name: String): Option[Session.Protocol_Handler] =
-    _protocol_handlers.get(name)
-
-
   /* theory files */
 
   def header_edit(name: Document.Node.Name, header: Document.Node.Header): Document.Edit_Text =
   {
     val header1 =

     def get: Prover = variable.value.get
     def set(p: Prover) { variable.change(_ => Some(p)) }
     def reset { variable.change(_ => None) }
     def await_reset() { variable.guarded_access({ case None => Some((), None) case _ => None }) }
   }
+
+
+  /* protocol handlers */
+
+  private val _protocol_handlers = Synchronized(new Session.Protocol_Handlers)
+
+  def get_protocol_handler(name: String): Option[Session.Protocol_Handler] =
+    _protocol_handlers.value.get(name)
+
+  def add_protocol_handler(name: String): Unit =
+    _protocol_handlers.change(_.add(prover.get, name))
 
 
   /* manager thread */
 
   private val delay_prune = Simple_Thread.delay_first(prune_delay) { manager.send(Prune_History) }

         }
       }
 
       output match {
         case msg: Prover.Protocol_Output =>
-          val handled = _protocol_handlers.invoke(msg)
+          val handled = _protocol_handlers.value.invoke(msg)
           if (!handled) {
             msg.properties match {
               case Markup.Protocol_Handler(name) if prover.defined =>
-                _protocol_handlers = _protocol_handlers.add(prover.get, name)
+                add_protocol_handler(name)
 
               case Protocol.Command_Timing(state_id, timing) if prover.defined =>
                 val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
                 accumulate(state_id, prover.get.xml_cache.elem(message))
 

               prover.set(resources.start_prover(manager.send(_), name, args))
             }
 
           case Stop =>
             if (prover.defined && is_ready) {
-              _protocol_handlers = _protocol_handlers.stop(prover.get)
+              _protocol_handlers.change(_.stop(prover.get))
               global_state.change(_ => Document.State.init)
               phase = Session.Shutdown
               prover.get.terminate
             }