--- a/src/Pure/System/command_line.scala Tue Apr 22 12:05:02 2014 +0200
+++ b/src/Pure/System/command_line.scala Tue Apr 22 12:30:54 2014 +0200
@@ -35,5 +35,7 @@
}
sys.exit(rc)
}
+
+ def tool0(body: => Unit): Nothing = tool { body; 0 }
}
--- a/src/Pure/System/options.scala Tue Apr 22 12:05:02 2014 +0200
+++ b/src/Pure/System/options.scala Tue Apr 22 12:30:54 2014 +0200
@@ -141,7 +141,7 @@
def main(args: Array[String])
{
- Command_Line.tool {
+ Command_Line.tool0 {
args.toList match {
case get_option :: export_file :: more_options =>
val options = (Options.init() /: more_options)(_ + _)
@@ -155,7 +155,6 @@
if (get_option == "" && export_file == "")
System.out.println(options.print)
- 0
case _ => error("Bad arguments:\n" + cat_lines(args))
}
}
--- a/src/Pure/Tools/build.ML Tue Apr 22 12:05:02 2014 +0200
+++ b/src/Pure/Tools/build.ML Tue Apr 22 12:30:54 2014 +0200
@@ -124,7 +124,7 @@
in
-fun build args_file = Command_Line.tool (fn () =>
+fun build args_file = Command_Line.tool0 (fn () =>
let
val _ = SHA1_Samples.test ();
@@ -167,7 +167,7 @@
val _ = Options.reset_default ();
val _ = if do_output then () else exit 0;
- in 0 end);
+ in () end);
end;
--- a/src/Pure/Tools/doc.scala Tue Apr 22 12:05:02 2014 +0200
+++ b/src/Pure/Tools/doc.scala Tue Apr 22 12:30:54 2014 +0200
@@ -90,7 +90,7 @@
def main(args: Array[String])
{
- Command_Line.tool {
+ Command_Line.tool0 {
val entries = contents()
if (args.isEmpty) Console.println(cat_lines(contents_lines().map(_._2)))
else {
@@ -101,7 +101,6 @@
}
)
}
- 0
}
}
}
--- a/src/Pure/Tools/keywords.scala Tue Apr 22 12:05:02 2014 +0200
+++ b/src/Pure/Tools/keywords.scala Tue Apr 22 12:30:54 2014 +0200
@@ -164,14 +164,12 @@
def main(args: Array[String])
{
- Command_Line.tool {
+ Command_Line.tool0 {
args.toList match {
case "keywords" :: name :: Command_Line.Chunks(dirs, sessions) =>
keywords(Options.init(), name, dirs.map(Path.explode), sessions)
- 0
case "update_keywords" :: Nil =>
update_keywords(Options.init())
- 0
case _ => error("Bad arguments:\n" + cat_lines(args))
}
}