# HG changeset patch
# User wenzelm
# Date 1585589951 -7200
# Node ID 3f02bc5a5a03eb45dd5abe69c15dcf14cae7a98f
# Parent  50425e4c3910d71a5ae0939093918d911a247369
more accurate treatment of errors;

diff -r 50425e4c3910 -r 3f02bc5a5a03 src/Pure/PIDE/protocol_message.scala
--- 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) =>
diff -r 50425e4c3910 -r 3f02bc5a5a03 src/Pure/System/command_line.ML
--- 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;
-
diff -r 50425e4c3910 -r 3f02bc5a5a03 src/Pure/System/isabelle_process.ML
--- 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;
 
diff -r 50425e4c3910 -r 3f02bc5a5a03 src/Pure/System/process_result.scala
--- 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))
 
diff -r 50425e4c3910 -r 3f02bc5a5a03 src/Pure/Tools/build.ML
--- 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;
diff -r 50425e4c3910 -r 3f02bc5a5a03 src/Pure/Tools/build.scala
--- 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 {