# HG changeset patch # User wenzelm # Date 1585590601 -7200 # Node ID c1bc38327bc21f7f925bbe260c645db860b0ec0a # Parent 3f02bc5a5a03eb45dd5abe69c15dcf14cae7a98f clarified signature; diff -r 3f02bc5a5a03 -r c1bc38327bc2 src/Doc/System/Environment.thy --- 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>\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 3f02bc5a5a03 -r c1bc38327bc2 src/Pure/Admin/build_history.scala --- 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 diff -r 3f02bc5a5a03 -r c1bc38327bc2 src/Pure/Admin/build_polyml.scala --- 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(""" diff -r 3f02bc5a5a03 -r c1bc38327bc2 src/Pure/Admin/build_release.scala --- 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 diff -r 3f02bc5a5a03 -r c1bc38327bc2 src/Pure/Admin/isabelle_cronjob.scala --- 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] diff -r 3f02bc5a5a03 -r c1bc38327bc2 src/Pure/ML/ml_console.scala --- 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) } } } diff -r 3f02bc5a5a03 -r c1bc38327bc2 src/Pure/System/command_line.ML --- 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; diff -r 3f02bc5a5a03 -r c1bc38327bc2 src/Pure/System/command_line.scala --- 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("; ") + "));" } diff -r 3f02bc5a5a03 -r c1bc38327bc2 src/Pure/System/isabelle_tool.scala --- 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 = diff -r 3f02bc5a5a03 -r c1bc38327bc2 src/Pure/Tools/build.scala --- 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) { diff -r 3f02bc5a5a03 -r c1bc38327bc2 src/Pure/Tools/profiling_report.scala --- 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 ...]