--- a/src/Doc/System/Environment.thy Mon Mar 30 19:39:11 2020 +0200
+++ b/src/Doc/System/Environment.thy Mon Mar 30 19:50:01 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 Mon Mar 30 19:39:11 2020 +0200
+++ b/src/Pure/Admin/build_history.scala Mon Mar 30 19:50:01 2020 +0200
@@ -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_polyml.scala Mon Mar 30 19:39:11 2020 +0200
+++ b/src/Pure/Admin/build_polyml.scala Mon Mar 30 19:50:01 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 Mon Mar 30 19:39:11 2020 +0200
+++ b/src/Pure/Admin/build_release.scala Mon Mar 30 19:50:01 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 Mon Mar 30 19:39:11 2020 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala Mon Mar 30 19:50:01 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/ML/ml_console.scala Mon Mar 30 19:39:11 2020 +0200
+++ b/src/Pure/ML/ml_console.scala Mon Mar 30 19:50:01 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/System/command_line.ML Mon Mar 30 19:39:11 2020 +0200
+++ b/src/Pure/System/command_line.ML Mon Mar 30 19:50:01 2020 +0200
@@ -7,8 +7,7 @@
signature COMMAND_LINE =
sig
exception EXIT of int
- val tool: (unit -> int) -> unit
- val tool0: (unit -> unit) -> unit
+ val tool: (unit -> unit) -> unit
end;
structure Command_Line: COMMAND_LINE =
@@ -20,11 +19,9 @@
Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
let
val rc =
- restore_attributes body ()
+ (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 Mon Mar 30 19:39:11 2020 +0200
+++ b/src/Pure/System/command_line.scala Mon Mar 30 19:50:01 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_tool.scala Mon Mar 30 19:39:11 2020 +0200
+++ b/src/Pure/System/isabelle_tool.scala Mon Mar 30 19:50:01 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/Tools/build.scala Mon Mar 30 19:39:11 2020 +0200
+++ b/src/Pure/Tools/build.scala Mon Mar 30 19:50:01 2020 +0200
@@ -276,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) {
--- a/src/Pure/Tools/profiling_report.scala Mon Mar 30 19:39:11 2020 +0200
+++ b/src/Pure/Tools/profiling_report.scala Mon Mar 30 19:50:01 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 ...]