more type-safe handler interface;
proper progress for Build.Handler;

--- a/src/Pure/PIDE/batch_session.scala	Wed Jan 14 16:27:19 2015 +0100
+++ b/src/Pure/PIDE/batch_session.scala	Wed Jan 14 17:24:55 2015 +0100
@@ -43,10 +43,12 @@
 
     val prover_session = new Session(resources)
 
+    val handler = new Build.Handler(progress, session)
+
     prover_session.phase_changed +=
       Session.Consumer[Session.Phase](getClass.getName) {
         case Session.Ready =>
-          prover_session.add_protocol_handler(Build.handler_name)
+          prover_session.add_protocol_handler(handler)
           val master_dir = session_info.dir
           val theories = session_info.theories.map({ case (_, opts, thys) => (opts, thys) })
           build_theories_result =
@@ -58,16 +60,6 @@
         case _ =>
       }
 
-    prover_session.all_messages +=
-      Session.Consumer[Prover.Message](getClass.getName) {
-        case msg: Prover.Output =>
-          msg.properties match {
-            case Markup.Loading_Theory(name) => progress.theory(session, name)
-            case _ =>
-          }
-        case _ =>
-      }
-
     prover_session.start("Isabelle", List("-r", "-q", parent_session))
 
     session_result.join

--- a/src/Pure/PIDE/markup.scala	Wed Jan 14 16:27:19 2015 +0100
+++ b/src/Pure/PIDE/markup.scala	Wed Jan 14 17:24:55 2015 +0100
@@ -458,11 +458,12 @@
       }
   }
 
+  val LOADING_THEORY = "loading_theory"
   object Loading_Theory
   {
     def unapply(props: Properties.T): Option[String] =
       props match {
-        case List((FUNCTION, "loading_theory"), (NAME, name)) => Some(name)
+        case List((FUNCTION, LOADING_THEORY), (NAME, name)) => Some(name)
         case _ => None
       }
   }

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

--- a/src/Pure/Tools/build.scala	Wed Jan 14 16:27:19 2015 +0100
+++ b/src/Pure/Tools/build.scala	Wed Jan 14 17:24:55 2015 +0100
@@ -1029,16 +1029,14 @@
 
   /* PIDE protocol */
 
-  val handler_name = "isabelle.Build$Handler"
-
   def build_theories(
     session: Session, master_dir: Path, theories: List[(Options, List[Path])]): Promise[Boolean] =
-      session.get_protocol_handler(handler_name) match {
+      session.get_protocol_handler(classOf[Handler].getName) match {
         case Some(handler: Handler) => handler.build_theories(session, master_dir, theories)
         case _ => error("Cannot invoke build_theories: bad protocol handler")
       }
 
-  class Handler extends Session.Protocol_Handler
+  class Handler(progress: Progress, session_name: String) extends Session.Protocol_Handler
   {
     private val pending = Synchronized(Map.empty[String, Promise[Boolean]])
 
@@ -1052,6 +1050,12 @@
       promise
     }
 
+    private def loading_theory(prover: Prover, msg: Prover.Protocol_Output): Boolean =
+      msg.properties match {
+        case Markup.Loading_Theory(name) => progress.theory(session_name, name); true
+        case _ => false
+      }
+
     private def build_theories_result(prover: Prover, msg: Prover.Protocol_Output): Boolean =
       msg.properties match {
         case Markup.Build_Theories_Result(id, ok) =>
@@ -1066,7 +1070,10 @@
     override def stop(prover: Prover): Unit =
       pending.change(promises => { for ((_, promise) <- promises) promise.cancel; Map.empty })
 
-    val functions = Map(Markup.BUILD_THEORIES_RESULT -> build_theories_result _)
+    val functions =
+      Map(
+        Markup.BUILD_THEORIES_RESULT -> build_theories_result _,
+        Markup.LOADING_THEORY -> loading_theory _)
   }
 }