diff -r e94df7f6b608 -r 6193bbbbe564 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Wed Jan 14 16:27:19 2015 +0100
+++ b/src/Pure/PIDE/session.scala	Wed Jan 14 17:24:55 2015 +0100
@@ -105,14 +105,20 @@
     val functions: Map[String, (Prover, Prover.Protocol_Output) => Boolean]
   }
 
+  def bad_protocol_handler(exn: Throwable, name: String): Unit =
+    Output.error_message(
+      "Failed to initialize protocol handler: " + quote(name) + "\n" + Exn.message(exn))
+
   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 add(prover: Prover, name: String): Protocol_Handlers =
+    def add(prover: Prover, handler: Protocol_Handler): Protocol_Handlers =
     {
+      val name = handler.getClass.getName
+
       val (handlers1, functions1) =
         handlers.get(name) match {
           case Some(old_handler) =>
@@ -124,22 +130,20 @@
 
       val (handlers2, functions2) =
         try {
-          val new_handler = Class.forName(name).newInstance.asInstanceOf[Protocol_Handler]
-          new_handler.start(prover)
+          handler.start(prover)
 
           val new_functions =
-            for ((a, f) <- new_handler.functions.toList) yield
+            for ((a, f) <- handler.functions.toList) yield
               (a, (msg: Prover.Protocol_Output) => f(prover, msg))
 
           val dups = for ((a, _) <- new_functions if functions1.isDefinedAt(a)) yield a
           if (dups.nonEmpty) error("Duplicate protocol functions: " + commas_quote(dups))
 
-          (handlers1 + (name -> new_handler), functions1 ++ new_functions)
+          (handlers1 + (name -> handler), functions1 ++ new_functions)
         }
         catch {
           case exn: Throwable =>
-            Output.error_message(
-              "Failed to initialize protocol handler: " + quote(name) + "\n" + Exn.message(exn))
+            Session.bad_protocol_handler(exn, name)
             (handlers1, functions1)
         }
 
@@ -342,8 +346,8 @@
   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))
+  def add_protocol_handler(handler: Session.Protocol_Handler): Unit =
+    _protocol_handlers.change(_.add(prover.get, handler))
 
 
   /* manager thread */
@@ -439,7 +443,12 @@
           if (!handled) {
             msg.properties match {
               case Markup.Protocol_Handler(name) if prover.defined =>
-                add_protocol_handler(name)
+                try {
+                  val handler =
+                    Class.forName(name).newInstance.asInstanceOf[Session.Protocol_Handler]
+                  add_protocol_handler(handler)
+                }
+                catch { case exn: Throwable => Session.bad_protocol_handler(exn, name) }
 
               case Protocol.Command_Timing(state_id, timing) if prover.defined =>
                 val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))