# HG changeset patch # User nipkow # Date 1585668414 -7200 # Node ID 03695eeabdde928d00849d5e4aa8afff7842a54e # Parent c1bc38327bc21f7f925bbe260c645db860b0ec0a# Parent 07bec530f02e36defc2644008c8a9d9ae5a80187 merged diff -r 07bec530f02e -r 03695eeabdde src/Doc/System/Environment.thy --- 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>\val it = (): unit\ result: - @{verbatim [display] \isabelle process -e 'Command_Line.tool0 (fn () => writeln "OK")'\} - @{verbatim [display] \isabelle process -e 'Command_Line.tool0 (fn () => error "Bad")'\} + @{verbatim [display] \isabelle process -e 'Command_Line.tool (fn () => writeln "OK")'\} + @{verbatim [display] \isabelle process -e 'Command_Line.tool (fn () => error "Bad")'\} \ diff -r 07bec530f02e -r 03695eeabdde src/Pure/Admin/build_history.scala --- 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 diff -r 07bec530f02e -r 03695eeabdde src/Pure/Admin/build_log.scala --- 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] = diff -r 07bec530f02e -r 03695eeabdde src/Pure/Admin/build_polyml.scala --- 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(""" diff -r 07bec530f02e -r 03695eeabdde src/Pure/Admin/build_release.scala --- 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 diff -r 07bec530f02e -r 03695eeabdde src/Pure/Admin/isabelle_cronjob.scala --- 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] diff -r 07bec530f02e -r 03695eeabdde src/Pure/Admin/jenkins.scala --- 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)) } } diff -r 07bec530f02e -r 03695eeabdde src/Pure/ML/ml_console.scala --- 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) } } } diff -r 07bec530f02e -r 03695eeabdde src/Pure/PIDE/protocol.scala --- 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( diff -r 07bec530f02e -r 03695eeabdde src/Pure/PIDE/protocol_message.scala --- 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) => diff -r 07bec530f02e -r 03695eeabdde src/Pure/System/command_line.ML --- 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; - diff -r 07bec530f02e -r 03695eeabdde src/Pure/System/command_line.scala --- 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("; ") + "));" } diff -r 07bec530f02e -r 03695eeabdde src/Pure/System/isabelle_process.ML --- 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; diff -r 07bec530f02e -r 03695eeabdde src/Pure/System/isabelle_tool.scala --- 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 = diff -r 07bec530f02e -r 03695eeabdde src/Pure/System/process_result.scala --- 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)) diff -r 07bec530f02e -r 03695eeabdde src/Pure/Tools/build.ML --- 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; diff -r 07bec530f02e -r 03695eeabdde src/Pure/Tools/build.scala --- 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 = diff -r 07bec530f02e -r 03695eeabdde src/Pure/Tools/profiling_report.scala --- 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 ...]