src/Pure/System/command_line.scala
author wenzelm
Wed, 08 Aug 2012 12:33:40 +0200
changeset 48731 a45ba78abcc1
parent 48346 e2382bede914
child 51980 fe16d1128a14
permissions -rw-r--r--
more casual exit back to ML toplevel, to accomodate commit in SML/NJ which continues at the saved point;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
48346
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/System/command_line.scala
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
     3
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
     4
Support for Isabelle/Scala command line tools.
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
     5
*/
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
     6
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
     7
package isabelle
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
     8
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
     9
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    10
object Command_Line
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    11
{
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    12
  object Chunks
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    13
  {
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    14
    private def chunks(list: List[String]): List[List[String]] =
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    15
      list.indexWhere(_ == "\n") match {
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    16
        case -1 => List(list)
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    17
        case i =>
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    18
          val (chunk, rest) = list.splitAt(i)
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    19
          chunk :: chunks(rest.tail)
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    20
      }
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    21
    def unapplySeq(list: List[String]): Option[List[List[String]]] = Some(chunks(list))
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    22
  }
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    23
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    24
  def tool(body: => Int): Nothing =
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    25
  {
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    26
    val rc =
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    27
      try { body }
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    28
      catch { case exn: Throwable => java.lang.System.err.println(Exn.message(exn)); 2 }
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    29
    sys.exit(rc)
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    30
  }
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    31
}
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    32