src/Pure/System/command_line.scala
changeset 48346 e2382bede914
child 51980 fe16d1128a14
--- /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)
+  }
+}
+