src/Pure/System/session.scala

 
   class Protocol_Handlers(
     handlers: Map[String, Session.Protocol_Handler] = Map.empty,
     functions: Map[String, Isabelle_Process.Output => Boolean] = Map.empty)
   {
+    def get(name: String): Option[Protocol_Handler] = handlers.get(name)
+
     def add(prover: Prover, name: String): Protocol_Handlers =
     {
       val (handlers1, functions1) =
         handlers.get(name) match {
           case Some(old_handler) =>

   def snapshot(name: Document.Node.Name = Document.Node.Name.empty,
       pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
     global_state().snapshot(name, pending_edits)
 
 
+  /* 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 =

   private case class Cancel_Exec(exec_id: Document_ID.Exec)
   private case class Change(
     doc_edits: List[Document.Edit_Command],
     previous: Document.Version,
     version: Document.Version)
+  private case class Protocol_Command(name: String, args: List[String])
   private case class Messages(msgs: List[Isabelle_Process.Message])
   private case class Update_Options(options: Options)
 
   private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
   {
     val this_actor = self
-
-    var protocol_handlers = new Session.Protocol_Handlers()
 
     var prune_next = System.currentTimeMillis() + prune_delay.ms
 
 
     /* buffered prover messages */

           case _: Document.State.Fail => bad_output()
         }
       }
 
       if (output.is_protocol) {
-        val handled = protocol_handlers.invoke(output)
+        val handled = _protocol_handlers.invoke(output)
         if (!handled) {
           output.properties match {
             case Markup.Protocol_Handler(name) =>
-              protocol_handlers = protocol_handlers.add(prover.get, name)
+              _protocol_handlers = _protocol_handlers.add(prover.get, name)
 
             case Protocol.Command_Timing(state_id, timing) =>
               val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
               accumulate(state_id, prover.get.xml_cache.elem(message))
 

             prover = Some(new Isabelle_Process(receiver.invoke _, args) with Protocol)
           }
 
         case Stop =>
           if (phase == Session.Ready) {
-            protocol_handlers = protocol_handlers.stop(prover.get)
+            _protocol_handlers = _protocol_handlers.stop(prover.get)
             global_state >> (_ => Document.State.init)  // FIXME event bus!?
             phase = Session.Shutdown
             prover.get.terminate
             prover = None
             phase = Session.Inactive

 
         case Session.Dialog_Result(id, serial, result) if prover.isDefined =>
           prover.get.dialog_result(serial, result)
           handle_output(new Isabelle_Process.Output(Protocol.Dialog_Result(id, serial, result)))
 
+        case Protocol_Command(name, args) if prover.isDefined =>
+          prover.get.protocol_command(name, args:_*)
+
         case Messages(msgs) =>
           msgs foreach {
             case input: Isabelle_Process.Input =>
               all_messages.event(input)
 

     commands_changed_buffer !? Stop
     change_parser !? Stop
     session_actor !? Stop
   }
 
+  def protocol_command(name: String, args: String*)
+  { session_actor ! Protocol_Command(name, args.toList) }
+
   def cancel_exec(exec_id: Document_ID.Exec) { session_actor ! Cancel_Exec(exec_id) }
 
   def update(edits: List[Document.Edit_Text])
   { if (!edits.isEmpty) session_actor !? Session.Raw_Edits(edits) }