--- a/src/Pure/System/build.scala Thu Jul 19 11:54:19 2012 +0200
+++ b/src/Pure/System/build.scala Thu Jul 19 12:05:54 2012 +0200
@@ -159,40 +159,22 @@
}
-
- /** command line entry point **/
-
- private object Chunks
- {
- private def chunks(list: List[String]): List[List[String]] =
- list.indexWhere(_ == "\n") match {
- case -1 => List(list)
- case i =>
- val (chunk, rest) = list.splitAt(i)
- chunk :: chunks(rest.tail)
- }
- def unapplySeq(list: List[String]): Option[List[List[String]]] = Some(chunks(list))
- }
+ /* command line entry point */
def main(args: Array[String])
{
- val rc =
- try {
- args.toList match {
- case
- Properties.Value.Boolean(all_sessions) ::
- Properties.Value.Boolean(build_images) ::
- Properties.Value.Boolean(list_only) ::
- Chunks(more_dirs, options, sessions) =>
- build(all_sessions, build_images, list_only,
- more_dirs.map(Path.explode), options, sessions)
- case _ => error("Bad arguments:\n" + cat_lines(args))
- }
+ Command_Line.tool {
+ args.toList match {
+ case
+ Properties.Value.Boolean(all_sessions) ::
+ Properties.Value.Boolean(build_images) ::
+ Properties.Value.Boolean(list_only) ::
+ Command_Line.Chunks(more_dirs, options, sessions) =>
+ build(all_sessions, build_images, list_only,
+ more_dirs.map(Path.explode), options, sessions)
+ case _ => error("Bad arguments:\n" + cat_lines(args))
}
- catch {
- case exn: Throwable => java.lang.System.err.println(Exn.message(exn)); 2
- }
- sys.exit(rc)
+ }
}
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/command_line.scala Thu Jul 19 12:05:54 2012 +0200
@@ -0,0 +1,32 @@
+/* Title: Pure/System/command_line.scala
+ Author: Makarius
+
+Support for Isabelle/Scala command line tools.
+*/
+
+package isabelle
+
+
+object Command_Line
+{
+ object Chunks
+ {
+ private def chunks(list: List[String]): List[List[String]] =
+ list.indexWhere(_ == "\n") match {
+ case -1 => List(list)
+ case i =>
+ val (chunk, rest) = list.splitAt(i)
+ chunk :: chunks(rest.tail)
+ }
+ def unapplySeq(list: List[String]): Option[List[List[String]]] = Some(chunks(list))
+ }
+
+ def tool(body: => Int): Nothing =
+ {
+ val rc =
+ try { body }
+ catch { case exn: Throwable => java.lang.System.err.println(Exn.message(exn)); 2 }
+ sys.exit(rc)
+ }
+}
+
--- a/src/Pure/build-jars Thu Jul 19 11:54:19 2012 +0200
+++ b/src/Pure/build-jars Thu Jul 19 12:05:54 2012 +0200
@@ -40,6 +40,7 @@
PIDE/xml.scala
PIDE/yxml.scala
System/build.scala
+ System/command_line.scala
System/event_bus.scala
System/gui_setup.scala
System/invoke_scala.scala