src/Pure/System/command_line.scala
author wenzelm
Mon Jul 15 10:25:35 2013 +0200 (2013-07-15 ago)
changeset 52655 3b2b1ef13979
parent 51980 fe16d1128a14
child 55618 995162143ef4
permissions -rw-r--r--
more careful termination of removed execs, leaving running execs undisturbed;
wenzelm@48346
     1
/*  Title:      Pure/System/command_line.scala
wenzelm@48346
     2
    Author:     Makarius
wenzelm@48346
     3
wenzelm@48346
     4
Support for Isabelle/Scala command line tools.
wenzelm@48346
     5
*/
wenzelm@48346
     6
wenzelm@48346
     7
package isabelle
wenzelm@48346
     8
wenzelm@48346
     9
wenzelm@48346
    10
object Command_Line
wenzelm@48346
    11
{
wenzelm@48346
    12
  object Chunks
wenzelm@48346
    13
  {
wenzelm@48346
    14
    private def chunks(list: List[String]): List[List[String]] =
wenzelm@48346
    15
      list.indexWhere(_ == "\n") match {
wenzelm@48346
    16
        case -1 => List(list)
wenzelm@48346
    17
        case i =>
wenzelm@48346
    18
          val (chunk, rest) = list.splitAt(i)
wenzelm@48346
    19
          chunk :: chunks(rest.tail)
wenzelm@48346
    20
      }
wenzelm@48346
    21
    def unapplySeq(list: List[String]): Option[List[List[String]]] = Some(chunks(list))
wenzelm@48346
    22
  }
wenzelm@48346
    23
wenzelm@51980
    24
  var debug = false
wenzelm@51980
    25
wenzelm@48346
    26
  def tool(body: => Int): Nothing =
wenzelm@48346
    27
  {
wenzelm@48346
    28
    val rc =
wenzelm@48346
    29
      try { body }
wenzelm@51980
    30
      catch {
wenzelm@51980
    31
        case exn: Throwable =>
wenzelm@51980
    32
          if (debug) exn.printStackTrace
wenzelm@51980
    33
          java.lang.System.err.println(Exn.message(exn))
wenzelm@51980
    34
          2
wenzelm@51980
    35
      }
wenzelm@48346
    36
    sys.exit(rc)
wenzelm@48346
    37
  }
wenzelm@48346
    38
}
wenzelm@48346
    39