--- a/src/Pure/Tools/build.scala Thu Jan 15 11:39:58 2015 +0100
+++ b/src/Pure/Tools/build.scala Thu Jan 15 12:54:08 2015 +0100
@@ -1030,7 +1030,7 @@
/* PIDE protocol */
def build_theories(
- session: Session, master_dir: Path, theories: List[(Options, List[Path])]): Promise[Boolean] =
+ session: Session, master_dir: Path, theories: List[(Options, List[Path])]): Promise[XML.Body] =
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")
@@ -1038,12 +1038,12 @@
class Handler(progress: Progress, session_name: String) extends Session.Protocol_Handler
{
- private val pending = Synchronized(Map.empty[String, Promise[Boolean]])
+ private val pending = Synchronized(Map.empty[String, Promise[XML.Body]])
def build_theories(
- session: Session, master_dir: Path, theories: List[(Options, List[Path])]): Promise[Boolean] =
+ session: Session, master_dir: Path, theories: List[(Options, List[Path])]): Promise[XML.Body] =
{
- val promise = Future.promise[Boolean]
+ val promise = Future.promise[XML.Body]
val id = Document_ID.make().toString
pending.change(promises => promises + (id -> promise))
session.build_theories(id, master_dir, theories)
@@ -1058,11 +1058,17 @@
private def build_theories_result(prover: Prover, msg: Prover.Protocol_Output): Boolean =
msg.properties match {
- case Markup.Build_Theories_Result(id, ok) =>
+ case Markup.Build_Theories_Result(id) =>
pending.change_result(promises =>
promises.get(id) match {
- case Some(promise) => promise.fulfill(ok); (true, promises - id)
- case None => (false, promises)
+ case Some(promise) =>
+ val error_message =
+ try { YXML.parse_body(Symbol.decode(msg.text)) }
+ catch { case exn: Throwable => List(XML.Text(Exn.message(exn))) }
+ promise.fulfill(error_message)
+ (true, promises - id)
+ case None =>
+ (false, promises)
})
case _ => false
}