# 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 }