--- 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 ...]