merged
authornipkow
Tue, 31 Mar 2020 17:26:54 +0200
changeset 71634 03695eeabdde
parent 71632 c1bc38327bc2 (diff)
parent 71633 07bec530f02e (current diff)
child 71635 b36f07d28867
merged
--- a/src/Doc/System/Environment.thy	Tue Mar 31 15:51:15 2020 +0200
+++ b/src/Doc/System/Environment.thy	Tue Mar 31 17:26:54 2020 +0200
@@ -390,8 +390,8 @@
   \<^medskip>
   This is how to invoke a function body with proper return code and printing
   of errors, and without printing of a redundant \<^verbatim>\<open>val it = (): unit\<close> result:
-  @{verbatim [display] \<open>isabelle process -e 'Command_Line.tool0 (fn () => writeln "OK")'\<close>}
-  @{verbatim [display] \<open>isabelle process -e 'Command_Line.tool0 (fn () => error "Bad")'\<close>}
+  @{verbatim [display] \<open>isabelle process -e 'Command_Line.tool (fn () => writeln "OK")'\<close>}
+  @{verbatim [display] \<open>isabelle process -e 'Command_Line.tool (fn () => error "Bad")'\<close>}
 \<close>
 
 
--- a/src/Pure/Admin/build_history.scala	Tue Mar 31 15:51:15 2020 +0200
+++ b/src/Pure/Admin/build_history.scala	Tue Mar 31 17:26:54 2020 +0200
@@ -281,7 +281,7 @@
                 val theory_timings =
                   try {
                     store.read_theory_timings(db, session_name).map(ps =>
-                      Build_Log.Theory_Timing_Marker((Build_Log.SESSION_NAME, session_name) :: ps))
+                      Protocol.Theory_Timing_Marker((Build_Log.SESSION_NAME, session_name) :: ps))
                   }
                   catch { case ERROR(_) => Nil }
 
@@ -355,10 +355,10 @@
       build_out_progress.echo("Writing log file " + log_path.ext("xz") + " ...")
       File.write_xz(log_path.ext("xz"),
         terminate_lines(
-          Build_Log.Meta_Info_Marker(meta_info) :: build_result.out_lines :::
+          Protocol.Meta_Info_Marker(meta_info) :: build_result.out_lines :::
           session_build_info :::
-          ml_statistics.map(Build_Log.ML_Statistics_Marker.apply) :::
-          session_errors.map(Build_Log.Error_Message_Marker.apply) :::
+          ml_statistics.map(Protocol.ML_Statistics_Marker.apply) :::
+          session_errors.map(Protocol.Error_Message_Marker.apply) :::
           heap_sizes), XZ.options(6))
 
 
@@ -393,7 +393,7 @@
 
   def main(args: Array[String])
   {
-    Command_Line.tool0 {
+    Command_Line.tool {
       var afp_rev: Option[String] = None
       var multicore_base = false
       var components_base: Path = Components.default_components_base
--- a/src/Pure/Admin/build_log.scala	Tue Mar 31 15:51:15 2020 +0200
+++ b/src/Pure/Admin/build_log.scala	Tue Mar 31 17:26:54 2020 +0200
@@ -387,8 +387,8 @@
     }
 
     log_file.lines match {
-      case line :: _ if Meta_Info_Marker.test_yxml(line) =>
-        Meta_Info(log_file.find_props(Meta_Info_Marker).get, log_file.get_all_settings)
+      case line :: _ if Protocol.Meta_Info_Marker.test_yxml(line) =>
+        Meta_Info(log_file.find_props(Protocol.Meta_Info_Marker).get, log_file.get_all_settings)
 
       case Identify.Start(log_file.Strict_Date(start)) :: _ =>
         parse(Identify.engine(log_file), "", start, Identify.No_End,
@@ -431,13 +431,6 @@
 
   /** build info: toplevel output of isabelle build or Admin/build_history **/
 
-  val Meta_Info_Marker = Protocol_Message.Marker("meta_info")
-  val Timing_Marker = Protocol_Message.Marker("Timing")
-  val Command_Timing_Marker = Protocol_Message.Marker("command_timing")
-  val Theory_Timing_Marker = Protocol_Message.Marker("theory_timing")
-  val ML_Statistics_Marker = Protocol_Message.Marker("ML_statistics")
-  val Task_Statistics_Marker = Protocol_Message.Marker("task_statistics")
-  val Error_Message_Marker = Protocol_Message.Marker("error_message")
   val SESSION_NAME = "session_name"
 
   object Session_Status extends Enumeration
@@ -503,7 +496,8 @@
     object Theory_Timing
     {
       def unapply(line: String): Option[(String, (String, Timing))] =
-        Theory_Timing_Marker.unapply(line.replace('~', '-')).map(log_file.parse_props) match {
+        Protocol.Theory_Timing_Marker.unapply(line.replace('~', '-')).map(log_file.parse_props)
+        match {
           case Some((SESSION_NAME, name) :: props) =>
             (props, props) match {
               case (Markup.Name(thy), Markup.Timing_Properties(t)) => Some((name, thy -> t))
@@ -572,22 +566,22 @@
         case Heap(name, Value.Long(size)) =>
           heap_sizes += (name -> size)
 
-        case _ if Theory_Timing_Marker.test_yxml(line) =>
+        case _ if Protocol.Theory_Timing_Marker.test_yxml(line) =>
           line match {
             case Theory_Timing(name, theory_timing) =>
               theory_timings += (name -> (theory_timings.getOrElse(name, Map.empty) + theory_timing))
             case _ => log_file.err("malformed theory_timing " + quote(line))
           }
 
-        case _ if parse_ml_statistics && ML_Statistics_Marker.test_yxml(line) =>
-          ML_Statistics_Marker.unapply(line).map(log_file.parse_props) match {
+        case _ if parse_ml_statistics && Protocol.ML_Statistics_Marker.test_yxml(line) =>
+          Protocol.ML_Statistics_Marker.unapply(line).map(log_file.parse_props) match {
             case Some((SESSION_NAME, name) :: props) =>
               ml_statistics += (name -> (props :: ml_statistics.getOrElse(name, Nil)))
             case _ => log_file.err("malformed ML_statistics " + quote(line))
           }
 
-        case _ if Error_Message_Marker.test_yxml(line) =>
-          Error_Message_Marker.unapply(line).map(log_file.parse_props) match {
+        case _ if Protocol.Error_Message_Marker.test_yxml(line) =>
+          Protocol.Error_Message_Marker.unapply(line).map(log_file.parse_props) match {
             case Some(List((SESSION_NAME, name), (Markup.CONTENT, msg))) =>
               errors += (name -> (msg :: errors.getOrElse(name, Nil)))
             case _ => log_file.err("malformed error message " + quote(line))
@@ -649,12 +643,16 @@
     task_statistics: Boolean): Session_Info =
   {
     Session_Info(
-      session_timing = log_file.find_props(Timing_Marker) getOrElse Nil,
-      command_timings = if (command_timings) log_file.filter_props(Command_Timing_Marker) else Nil,
-      theory_timings = if (theory_timings) log_file.filter_props(Theory_Timing_Marker) else Nil,
-      ml_statistics = if (ml_statistics) log_file.filter_props(ML_Statistics_Marker) else Nil,
-      task_statistics = if (task_statistics) log_file.filter_props(Task_Statistics_Marker) else Nil,
-      errors = log_file.filter(Error_Message_Marker))
+      session_timing = log_file.find_props(Protocol.Timing_Marker) getOrElse Nil,
+      command_timings =
+        if (command_timings) log_file.filter_props(Protocol.Command_Timing_Marker) else Nil,
+      theory_timings =
+        if (theory_timings) log_file.filter_props(Protocol.Theory_Timing_Marker) else Nil,
+      ml_statistics =
+        if (ml_statistics) log_file.filter_props(Protocol.ML_Statistics_Marker) else Nil,
+      task_statistics =
+        if (task_statistics) log_file.filter_props(Protocol.Task_Statistics_Marker) else Nil,
+      errors = log_file.filter(Protocol.Error_Message_Marker))
   }
 
   def compress_errors(errors: List[String], cache: XZ.Cache = XZ.cache()): Option[Bytes] =
--- a/src/Pure/Admin/build_polyml.scala	Tue Mar 31 15:51:15 2020 +0200
+++ b/src/Pure/Admin/build_polyml.scala	Tue Mar 31 17:26:54 2020 +0200
@@ -256,7 +256,7 @@
   val isabelle_tool1 =
     Isabelle_Tool("build_polyml", "build Poly/ML from sources", args =>
     {
-      Command_Line.tool0 {
+      Command_Line.tool {
         var msys_root: Option[Path] = None
         var arch_64 = false
         var sha1_root: Option[Path] = None
@@ -295,7 +295,7 @@
   val isabelle_tool2 =
     Isabelle_Tool("build_polyml_component", "make skeleton for Poly/ML component", args =>
     {
-      Command_Line.tool0 {
+      Command_Line.tool {
         var sha1_root: Option[Path] = None
 
         val getopts = Getopts("""
--- a/src/Pure/Admin/build_release.scala	Tue Mar 31 15:51:15 2020 +0200
+++ b/src/Pure/Admin/build_release.scala	Tue Mar 31 17:26:54 2020 +0200
@@ -775,7 +775,7 @@
 
   def main(args: Array[String])
   {
-    Command_Line.tool0 {
+    Command_Line.tool {
       var afp_rev = ""
       var components_base: Path = Components.default_components_base
       var official_release = false
--- a/src/Pure/Admin/isabelle_cronjob.scala	Tue Mar 31 15:51:15 2020 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Tue Mar 31 17:26:54 2020 +0200
@@ -579,7 +579,7 @@
 
   def main(args: Array[String])
   {
-    Command_Line.tool0 {
+    Command_Line.tool {
       var force = false
       var verbose = false
       var exclude_task = Set.empty[String]
--- a/src/Pure/Admin/jenkins.scala	Tue Mar 31 15:51:15 2020 +0200
+++ b/src/Pure/Admin/jenkins.scala	Tue Mar 31 17:26:54 2020 +0200
@@ -112,7 +112,7 @@
 
         File.write_xz(log_path,
           terminate_lines(Url.read(main_log) ::
-            ml_statistics.map(Build_Log.ML_Statistics_Marker.apply)),
+            ml_statistics.map(Protocol.ML_Statistics_Marker.apply)),
           XZ.options(6))
       }
     }
--- a/src/Pure/ML/ml_console.scala	Tue Mar 31 15:51:15 2020 +0200
+++ b/src/Pure/ML/ml_console.scala	Tue Mar 31 17:26:54 2020 +0200
@@ -81,7 +81,9 @@
         rc
       }
       tty_loop.join
-      process_result.join
+
+      val rc = process_result.join
+      if (rc != 0) sys.exit(rc)
     }
   }
 }
--- a/src/Pure/PIDE/protocol.scala	Tue Mar 31 15:51:15 2020 +0200
+++ b/src/Pure/PIDE/protocol.scala	Tue Mar 31 17:26:54 2020 +0200
@@ -9,6 +9,19 @@
 
 object Protocol
 {
+  /* markers for inlined messages */
+
+  val Loading_Theory_Marker = Protocol_Message.Marker("loading_theory")
+  val Export_Marker = Protocol_Message.Marker("export")
+  val Meta_Info_Marker = Protocol_Message.Marker("meta_info")
+  val Timing_Marker = Protocol_Message.Marker("Timing")
+  val Command_Timing_Marker = Protocol_Message.Marker("command_timing")
+  val Theory_Timing_Marker = Protocol_Message.Marker("theory_timing")
+  val ML_Statistics_Marker = Protocol_Message.Marker("ML_statistics")
+  val Task_Statistics_Marker = Protocol_Message.Marker("task_statistics")
+  val Error_Message_Marker = Protocol_Message.Marker("error_message")
+
+
   /* document editing */
 
   object Commands_Accepted
@@ -161,8 +174,6 @@
 
   /* export */
 
-  val Export_Marker = Protocol_Message.Marker(Markup.EXPORT)
-
   object Export
   {
     sealed case class Args(
--- a/src/Pure/PIDE/protocol_message.scala	Tue Mar 31 15:51:15 2020 +0200
+++ b/src/Pure/PIDE/protocol_message.scala	Tue Mar 31 17:26:54 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	Tue Mar 31 15:51:15 2020 +0200
+++ b/src/Pure/System/command_line.ML	Tue Mar 31 17:26:54 2020 +0200
@@ -6,22 +6,22 @@
 
 signature COMMAND_LINE =
 sig
-  val tool: (unit -> int) -> unit
-  val tool0: (unit -> unit) -> unit
+  exception EXIT of int
+  val tool: (unit -> unit) -> unit
 end;
 
 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 (); 0)
+          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/command_line.scala	Tue Mar 31 15:51:15 2020 +0200
+++ b/src/Pure/System/command_line.scala	Tue Mar 31 17:26:54 2020 +0200
@@ -23,10 +23,10 @@
 
   var debug = false
 
-  def tool(body: => Int): Nothing =
+  def tool(body: => Unit): Nothing =
   {
     val rc =
-      try { body }
+      try { body; 0 }
       catch {
         case exn: Throwable =>
           Output.error_message(Exn.message(exn) + (if (debug) "\n" + Exn.trace(exn) else ""))
@@ -35,8 +35,6 @@
     sys.exit(rc)
   }
 
-  def tool0(body: => Unit): Nothing = tool { body; 0 }
-
-  def ML_tool0(body: List[String]): String =
-    "Command_Line.tool0 (fn () => (" + body.mkString("; ") + "));"
+  def ML_tool(body: List[String]): String =
+    "Command_Line.tool (fn () => (" + body.mkString("; ") + "));"
 }
--- a/src/Pure/System/isabelle_process.ML	Tue Mar 31 15:51:15 2020 +0200
+++ b/src/Pure/System/isabelle_process.ML	Tue Mar 31 17:26:54 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/isabelle_tool.scala	Tue Mar 31 15:51:15 2020 +0200
+++ b/src/Pure/System/isabelle_tool.scala	Tue Mar 31 17:26:54 2020 +0200
@@ -108,7 +108,7 @@
   private def find_internal(name: String): Option[List[String] => Unit] =
     internal_tools.collectFirst({
       case tool if tool.name == name =>
-        args => Command_Line.tool0 { tool.body(args) }
+        args => Command_Line.tool { tool.body(args) }
       })
 
 
@@ -116,7 +116,7 @@
 
   def main(args: Array[String])
   {
-    Command_Line.tool0 {
+    Command_Line.tool {
       args.toList match {
         case Nil | List("-?") =>
           val tool_descriptions =
--- a/src/Pure/System/process_result.scala	Tue Mar 31 15:51:15 2020 +0200
+++ b/src/Pure/System/process_result.scala	Tue Mar 31 17:26:54 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	Tue Mar 31 15:51:15 2020 +0200
+++ b/src/Pure/Tools/build.ML	Tue Mar 31 17:26:54 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	Tue Mar 31 15:51:15 2020 +0200
+++ b/src/Pure/Tools/build.scala	Tue Mar 31 17:26:54 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
     }
@@ -184,8 +187,6 @@
 
   /* job: running prover process */
 
-  private val Loading_Theory_Marker = Protocol_Message.Marker("loading_theory")
-
   private class Job(progress: Progress,
     name: String,
     val info: Sessions.Info,
@@ -262,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 {
@@ -275,7 +276,7 @@
           File.write(args_file, args_yxml)
 
           val eval_build = "Build.build " + ML_Syntax.print_string_bytes(File.standard_path(args_file))
-          val eval = Command_Line.ML_tool0(eval_build :: eval_store)
+          val eval = Command_Line.ML_tool(eval_build :: eval_store)
 
           val process =
             if (is_pure) {
@@ -294,7 +295,7 @@
           process.result(
             progress_stdout =
               {
-                case Loading_Theory_Marker(theory) =>
+                case Protocol.Loading_Theory_Marker(theory) =>
                   progress.theory(Progress.Theory(theory, session = name))
                 case Protocol.Export.Marker((args, path)) =>
                   val body =
--- a/src/Pure/Tools/profiling_report.scala	Tue Mar 31 15:51:15 2020 +0200
+++ b/src/Pure/Tools/profiling_report.scala	Tue Mar 31 17:26:54 2020 +0200
@@ -32,7 +32,7 @@
   val isabelle_tool =
     Isabelle_Tool("profiling_report", "report Poly/ML profiling information from log files", args =>
     {
-      Command_Line.tool0 {
+      Command_Line.tool {
         val getopts =
           Getopts("""
 Usage: isabelle profiling_report [LOGS ...]