1.1 --- a/src/Pure/System/build.scala	Thu Jul 19 11:54:19 2012 +0200
     1.2 +++ b/src/Pure/System/build.scala	Thu Jul 19 12:05:54 2012 +0200
     1.3 @@ -159,40 +159,22 @@
     1.4    }
     1.5  
     1.6  
     1.7 -
     1.8 -  /** command line entry point **/
     1.9 -
    1.10 -  private object Chunks
    1.11 -  {
    1.12 -    private def chunks(list: List[String]): List[List[String]] =
    1.13 -      list.indexWhere(_ == "\n") match {
    1.14 -        case -1 => List(list)
    1.15 -        case i =>
    1.16 -          val (chunk, rest) = list.splitAt(i)
    1.17 -          chunk :: chunks(rest.tail)
    1.18 -      }
    1.19 -    def unapplySeq(list: List[String]): Option[List[List[String]]] = Some(chunks(list))
    1.20 -  }
    1.21 +  /* command line entry point */
    1.22  
    1.23    def main(args: Array[String])
    1.24    {
    1.25 -    val rc =
    1.26 -      try {
    1.27 -        args.toList match {
    1.28 -          case
    1.29 -            Properties.Value.Boolean(all_sessions) ::
    1.30 -            Properties.Value.Boolean(build_images) ::
    1.31 -            Properties.Value.Boolean(list_only) ::
    1.32 -            Chunks(more_dirs, options, sessions) =>
    1.33 -              build(all_sessions, build_images, list_only,
    1.34 -                more_dirs.map(Path.explode), options, sessions)
    1.35 -          case _ => error("Bad arguments:\n" + cat_lines(args))
    1.36 -        }
    1.37 +    Command_Line.tool {
    1.38 +      args.toList match {
    1.39 +        case
    1.40 +          Properties.Value.Boolean(all_sessions) ::
    1.41 +          Properties.Value.Boolean(build_images) ::
    1.42 +          Properties.Value.Boolean(list_only) ::
    1.43 +          Command_Line.Chunks(more_dirs, options, sessions) =>
    1.44 +            build(all_sessions, build_images, list_only,
    1.45 +              more_dirs.map(Path.explode), options, sessions)
    1.46 +        case _ => error("Bad arguments:\n" + cat_lines(args))
    1.47        }
    1.48 -      catch {
    1.49 -        case exn: Throwable => java.lang.System.err.println(Exn.message(exn)); 2
    1.50 -      }
    1.51 -    sys.exit(rc)
    1.52 +    }
    1.53    }
    1.54  }
    1.55  

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/System/command_line.scala	Thu Jul 19 12:05:54 2012 +0200
     2.3 @@ -0,0 +1,32 @@
     2.4 +/*  Title:      Pure/System/command_line.scala
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Support for Isabelle/Scala command line tools.
     2.8 +*/
     2.9 +
    2.10 +package isabelle
    2.11 +
    2.12 +
    2.13 +object Command_Line
    2.14 +{
    2.15 +  object Chunks
    2.16 +  {
    2.17 +    private def chunks(list: List[String]): List[List[String]] =
    2.18 +      list.indexWhere(_ == "\n") match {
    2.19 +        case -1 => List(list)
    2.20 +        case i =>
    2.21 +          val (chunk, rest) = list.splitAt(i)
    2.22 +          chunk :: chunks(rest.tail)
    2.23 +      }
    2.24 +    def unapplySeq(list: List[String]): Option[List[List[String]]] = Some(chunks(list))
    2.25 +  }
    2.26 +
    2.27 +  def tool(body: => Int): Nothing =
    2.28 +  {
    2.29 +    val rc =
    2.30 +      try { body }
    2.31 +      catch { case exn: Throwable => java.lang.System.err.println(Exn.message(exn)); 2 }
    2.32 +    sys.exit(rc)
    2.33 +  }
    2.34 +}
    2.35 +

     3.1 --- a/src/Pure/build-jars	Thu Jul 19 11:54:19 2012 +0200
     3.2 +++ b/src/Pure/build-jars	Thu Jul 19 12:05:54 2012 +0200
     3.3 @@ -40,6 +40,7 @@
     3.4    PIDE/xml.scala
     3.5    PIDE/yxml.scala
     3.6    System/build.scala
     3.7 +  System/command_line.scala
     3.8    System/event_bus.scala
     3.9    System/gui_setup.scala
    3.10    System/invoke_scala.scala