src/Pure/System/command_line.scala
author wenzelm
Thu, 14 Aug 2014 16:20:14 +0200
changeset 57942 e5bec882fdd0
parent 56782 433cf57550fa
child 68806 4597812d5182
permissions -rw-r--r--
more informative Token.Fact: retain name of dynamic fact (without selection);
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
51980
fe16d1128a14 support for more informative crashes;
wenzelm
parents: 48346
diff changeset
    24
  var debug = false
fe16d1128a14 support for more informative crashes;
wenzelm
parents: 48346
diff changeset
    25
48346
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    26
  def tool(body: => Int): Nothing =
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    27
  {
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    28
    val rc =
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    29
      try { body }
51980
fe16d1128a14 support for more informative crashes;
wenzelm
parents: 48346
diff changeset
    30
      catch {
fe16d1128a14 support for more informative crashes;
wenzelm
parents: 48346
diff changeset
    31
        case exn: Throwable =>
fe16d1128a14 support for more informative crashes;
wenzelm
parents: 48346
diff changeset
    32
          if (debug) exn.printStackTrace
56782
433cf57550fa more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents: 56671
diff changeset
    33
          Output.error_message(Exn.message(exn))
56669
f42717b5dc84 clarified message and return code, in accordance to ML version;
wenzelm
parents: 56631
diff changeset
    34
          Exn.return_code(exn, 2)
51980
fe16d1128a14 support for more informative crashes;
wenzelm
parents: 48346
diff changeset
    35
      }
48346
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    36
    sys.exit(rc)
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    37
  }
56631
wenzelm
parents: 55618
diff changeset
    38
wenzelm
parents: 55618
diff changeset
    39
  def tool0(body: => Unit): Nothing = tool { body; 0 }
48346
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    40
}
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    41