--- a/src/Pure/PIDE/protocol_message.scala Mon Mar 30 11:59:44 2020 +0200
+++ b/src/Pure/PIDE/protocol_message.scala Mon Mar 30 19:39:11 2020 +0200
@@ -53,6 +53,14 @@
case t => t
}
+ def expose_no_reports(body: XML.Body): XML.Body =
+ body flatMap {
+ case XML.Wrapped_Elem(markup, body, ts) => List(XML.Wrapped_Elem(markup, body, expose_no_reports(ts)))
+ case XML.Elem(Markup(Markup.NO_REPORT, _), ts) => ts
+ case XML.Elem(markup, ts) => List(XML.Elem(markup, expose_no_reports(ts)))
+ case t => List(t)
+ }
+
def reports(props: Properties.T, body: XML.Body): List[XML.Elem] =
body flatMap {
case XML.Wrapped_Elem(Markup(Markup.REPORT, ps), body, ts) =>
--- a/src/Pure/System/command_line.ML Mon Mar 30 11:59:44 2020 +0200
+++ b/src/Pure/System/command_line.ML Mon Mar 30 19:39:11 2020 +0200
@@ -6,6 +6,7 @@
signature COMMAND_LINE =
sig
+ exception EXIT of int
val tool: (unit -> int) -> unit
val tool0: (unit -> unit) -> unit
end;
@@ -13,15 +14,17 @@
structure Command_Line: COMMAND_LINE =
struct
+exception EXIT of int;
+
fun tool body =
Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
let
val rc =
- restore_attributes body () handle exn =>
- Exn.capture_exit 2 (fn () => (Runtime.exn_error_message exn; raise exn)) ();
+ restore_attributes body ()
+ handle EXIT rc => rc
+ | exn => Exn.capture_exit 2 (fn () => (Runtime.exn_error_message exn; raise exn)) ();
in exit rc end) ();
fun tool0 body = tool (fn () => (body (); 0));
end;
-
--- a/src/Pure/System/isabelle_process.ML Mon Mar 30 11:59:44 2020 +0200
+++ b/src/Pure/System/isabelle_process.ML Mon Mar 30 19:39:11 2020 +0200
@@ -9,6 +9,7 @@
val is_active: unit -> bool
val protocol_command: string -> (string list -> unit) -> unit
val reset_tracing: Document_ID.exec -> unit
+ exception EXIT of exn
val crashes: exn list Synchronized.var
val init_options: unit -> unit
val init_options_interactive: unit -> unit
@@ -143,6 +144,8 @@
(* protocol loop -- uninterruptible *)
+exception EXIT of exn;
+
val crashes = Synchronized.var "Isabelle_Process.crashes" ([]: exn list);
local
@@ -152,6 +155,8 @@
Output.physical_stderr
"Recovered from Isabelle process crash -- see also Isabelle_Process.crashes\n");
+fun shutdown () = (Future.shutdown (); ignore (Execution.reset ()));
+
in
fun loop stream =
@@ -161,11 +166,9 @@
NONE => false
| SOME [] => (Output.system_message "Isabelle process: no input"; true)
| SOME (name :: args) => (run_command name args; true))
- handle exn => (Runtime.exn_system_message exn handle crash => recover crash; true);
- in
- if continue then loop stream
- else (Future.shutdown (); Execution.reset (); ())
- end;
+ handle EXIT exn => (shutdown (); Exn.reraise exn)
+ | exn => (Runtime.exn_system_message exn handle crash => recover crash; true);
+ in if continue then loop stream else shutdown () end;
end;
--- a/src/Pure/System/process_result.scala Mon Mar 30 11:59:44 2020 +0200
+++ b/src/Pure/System/process_result.scala Mon Mar 30 19:39:11 2020 +0200
@@ -15,6 +15,8 @@
{
def out: String = cat_lines(out_lines)
def err: String = cat_lines(err_lines)
+
+ def output(outs: List[String]): Process_Result = copy(out_lines = out_lines ::: outs)
def errors(errs: List[String]): Process_Result = copy(err_lines = err_lines ::: errs)
def error(err: String): Process_Result = errors(List(err))
--- a/src/Pure/Tools/build.ML Mon Mar 30 11:59:44 2020 +0200
+++ b/src/Pure/Tools/build.ML Mon Mar 30 19:39:11 2020 +0200
@@ -220,11 +220,13 @@
if name = Context.PureN then Theory.install_pure (Thy_Info.get_theory Context.PureN) else ();
in () end;
+
+(* command-line tool *)
+
fun inline_errors exn =
Runtime.exn_message_list exn
|> List.app (fn msg => Protocol_Message.marker_text "error_message" (YXML.content_of msg));
-(*command-line tool*)
fun build args_file =
let
val _ = SHA1.test_samples ();
@@ -239,16 +241,26 @@
val _ = Options.reset_default ();
in () end;
-(*PIDE version*)
+
+(* PIDE version *)
+
+fun build_session_finished errs =
+ XML.Encode.list XML.Encode.string errs
+ |> Output.protocol_message Markup.build_session_finished;
+
val _ =
Isabelle_Process.protocol_command "build_session"
(fn [args_yxml] =>
let
val args = decode_args args_yxml;
- val result = (build_session args; "") handle exn =>
- (Runtime.exn_message exn handle _ (*sic!*) =>
- "Exception raised, but failed to print details!");
- in Output.protocol_message Markup.build_session_finished [XML.Text result] end
+ val errs =
+ Future.interruptible_task (fn () =>
+ (build_session args; []) handle exn =>
+ (Runtime.exn_message_list exn handle _ (*sic!*) =>
+ (build_session_finished ["CRASHED"];
+ raise Isabelle_Process.EXIT exn))) ();
+ val _ = build_session_finished errs;
+ in if null errs then () else raise Isabelle_Process.EXIT (Command_Line.EXIT 1) end
| _ => raise Match);
end;
--- a/src/Pure/Tools/build.scala Mon Mar 30 11:59:44 2020 +0200
+++ b/src/Pure/Tools/build.scala Mon Mar 30 19:39:11 2020 +0200
@@ -153,16 +153,19 @@
class Handler(progress: Progress, session: Session, session_name: String)
extends Session.Protocol_Handler
{
- val result_error: Promise[String] = Future.promise
+ val build_session_errors: Promise[List[String]] = Future.promise
- override def exit() { result_error.cancel }
+ override def exit() { build_session_errors.cancel }
private def build_session_finished(msg: Prover.Protocol_Output): Boolean =
{
- val error_message =
- try { Pretty.string_of(Symbol.decode_yxml(msg.text)) }
- catch { case ERROR(msg) => msg }
- result_error.fulfill(error_message)
+ val errors =
+ try {
+ XML.Decode.list(x => x)(Symbol.decode_yxml(msg.text)).
+ map(err => Pretty.string_of(Protocol_Message.expose_no_reports(err)))
+ }
+ catch { case ERROR(err) => List(err) }
+ build_session_errors.fulfill(errors)
session.send_stop()
true
}
@@ -260,12 +263,12 @@
session.protocol_command("build_session", args_yxml)
val result = process.join
- handler.result_error.join match {
- case "" => result
- case msg =>
- result.copy(
- rc = result.rc max 1,
- out_lines = result.out_lines ::: split_lines(Output.error_message_text(msg)))
+ handler.build_session_errors.join match {
+ case Nil => result
+ case errors =>
+ result.error_rc.output(
+ errors.flatMap(s => split_lines(Output.error_message_text(s))) :::
+ errors.map(Protocol.Error_Message_Marker.apply))
}
}
else {