# HG changeset patch
# User wenzelm
# Date 1342692354 -7200
# Node ID e2382bede914556042b34a7d88ea7f9150d70dcd
# Parent  baec6226edd830616b06fa8629cac7d91c8a29a3
more general support for Isabelle/Scala command line tools;

diff -r baec6226edd8 -r e2382bede914 src/Pure/System/build.scala
--- 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)
+    }
   }
 }
 
diff -r baec6226edd8 -r e2382bede914 src/Pure/System/command_line.scala
--- /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)
+  }
+}
+
diff -r baec6226edd8 -r e2382bede914 src/Pure/build-jars
--- 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