# HG changeset patch
# User wenzelm
# Date 1421322848 -3600
# Node ID 7090199d3f788966028f265cf0f45a09740b71ff
# Parent  100db5cf5be545c6fda83820e8ba70b69a3dc132
more informative build_theories_result: cumulative Runtime.exn_message;

diff -r 100db5cf5be5 -r 7090199d3f78 src/Pure/PIDE/batch_session.scala
--- a/src/Pure/PIDE/batch_session.scala	Thu Jan 15 11:39:58 2015 +0100
+++ b/src/Pure/PIDE/batch_session.scala	Thu Jan 15 12:54:08 2015 +0100
@@ -16,7 +16,7 @@
     options: Options,
     verbose: Boolean = false,
     dirs: List[Path] = Nil,
-    session: String): Boolean =
+    session: String): Batch_Session =
   {
     val (_, session_tree) =
       Build.find_sessions(options, dirs).selection(false, false, Nil, List(session))
@@ -38,10 +38,8 @@
 
     val progress = new Build.Console_Progress(verbose)
 
-    val session_result = Future.promise[Unit]
-    @volatile var build_theories_result: Option[Promise[Boolean]] = None
-
     val prover_session = new Session(resources)
+    val batch_session = new Batch_Session(prover_session)
 
     val handler = new Build.Handler(progress, session)
 
@@ -51,22 +49,24 @@
           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 =
+          batch_session.build_theories_result =
             Some(Build.build_theories(prover_session, master_dir, theories))
         case Session.Inactive | Session.Failed =>
-          session_result.fulfill_result(Exn.Exn(ERROR("Prover process terminated")))
+          batch_session.session_result.fulfill_result(Exn.Exn(ERROR("Prover process terminated")))
         case Session.Shutdown =>
-          session_result.fulfill(())
+          batch_session.session_result.fulfill(())
         case _ =>
       }
 
     prover_session.start("Isabelle", List("-r", "-q", parent_session))
 
-    session_result.join
-    build_theories_result match {
-      case None => false
-      case Some(promise) => promise.join
-    }
+    batch_session
   }
 }
 
+class Batch_Session private(val session: Session)
+{
+  val session_result = Future.promise[Unit]
+  @volatile var build_theories_result: Option[Promise[XML.Body]] = None
+}
+
diff -r 100db5cf5be5 -r 7090199d3f78 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Thu Jan 15 11:39:58 2015 +0100
+++ b/src/Pure/PIDE/markup.ML	Thu Jan 15 12:54:08 2015 +0100
@@ -186,7 +186,7 @@
   val command_timing: Properties.entry
   val loading_theory: string -> Properties.T
   val dest_loading_theory: Properties.T -> string option
-  val build_theories_result: string -> bool -> Properties.T
+  val build_theories_result: string -> Properties.T
   val print_operationsN: string
   val print_operations: Properties.T
   val simp_trace_panelN: string
@@ -597,8 +597,7 @@
 fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name
   | dest_loading_theory _ = NONE;
 
-fun build_theories_result id ok =
-  [("function", "build_theories_result"), ("id", id), ("ok", print_bool ok)];
+fun build_theories_result id = [("function", "build_theories_result"), ("id", id)];
 
 val print_operationsN = "print_operations";
 val print_operations = [(functionN, print_operationsN)];
diff -r 100db5cf5be5 -r 7090199d3f78 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Thu Jan 15 11:39:58 2015 +0100
+++ b/src/Pure/PIDE/markup.scala	Thu Jan 15 12:54:08 2015 +0100
@@ -471,10 +471,9 @@
   val BUILD_THEORIES_RESULT = "build_theories_result"
   object Build_Theories_Result
   {
-    def unapply(props: Properties.T): Option[(String, Boolean)] =
+    def unapply(props: Properties.T): Option[String] =
       props match {
-        case List((FUNCTION, BUILD_THEORIES_RESULT),
-          ("id", id), ("ok", Properties.Value.Boolean(ok))) => Some((id, ok))
+        case List((FUNCTION, BUILD_THEORIES_RESULT), ("id", id)) => Some(id)
         case _ => None
       }
   }
diff -r 100db5cf5be5 -r 7090199d3f78 src/Pure/PIDE/session.ML
--- a/src/Pure/PIDE/session.ML	Thu Jan 15 11:39:58 2015 +0100
+++ b/src/Pure/PIDE/session.ML	Thu Jan 15 12:54:08 2015 +0100
@@ -11,6 +11,7 @@
   val get_keywords: unit -> Keyword.keywords
   val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
     (Path.T * Path.T) list -> string -> string * string -> bool -> unit
+  val shutdown: unit -> unit
   val finish: unit -> unit
   val save: string -> unit
   val protocol_handler: string -> unit
@@ -58,22 +59,23 @@
 
 (* finish *)
 
+fun shutdown () =
+ (Execution.shutdown ();
+  Event_Timer.shutdown ();
+  Future.shutdown ());
+
 fun finish () =
- (Execution.shutdown ();
+ (shutdown ();
   Thy_Info.finish ();
   Present.finish ();
-  Future.shutdown ();
-  Event_Timer.shutdown ();
-  Future.shutdown ();
+  shutdown ();
   keywords :=
     fold (curry Keyword.merge_keywords o Thy_Header.get_keywords o Thy_Info.get_theory)
       (Thy_Info.get_names ()) Keyword.empty_keywords;
   session_finished := true);
 
 fun save heap =
- (Execution.shutdown ();
-  Event_Timer.shutdown ();
-  Future.shutdown ();
+ (shutdown ();
   ML_System.share_common_data ();
   ML_System.save_state heap);
 
diff -r 100db5cf5be5 -r 7090199d3f78 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Thu Jan 15 11:39:58 2015 +0100
+++ b/src/Pure/Tools/build.ML	Thu Jan 15 12:54:08 2015 +0100
@@ -174,13 +174,14 @@
           YXML.parse_body theories_yxml |>
             let open XML.Decode
             in list (pair Options.decode (list (string #> rpair Position.none))) end;
-        val result =
+        val res1 =
           Exn.capture (fn () =>
             theories |> List.app (build_theories (K NONE) (Path.explode master_dir))) ();
-        val ok =
-          (case result of
-            Exn.Res _ => true
-          | Exn.Exn exn => (Runtime.exn_error_message exn; false));
-    in Output.protocol_message (Markup.build_theories_result id ok) [] end);
+        val res2 = Exn.capture Session.shutdown ();
+        val result =
+          (Par_Exn.release_all [res1, res2]; "") handle exn =>
+            (Runtime.exn_message exn handle _ (*sic!*) =>
+              "Exception raised, but failed to print details!");
+    in Output.protocol_message (Markup.build_theories_result id) [result] end);
 
 end;
diff -r 100db5cf5be5 -r 7090199d3f78 src/Pure/Tools/build.scala
--- 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
       }