--- 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
+}
+
--- 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)];
--- 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
}
}
--- 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);
--- 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;
--- 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
}