src/Pure/System/command_line.scala
author wenzelm
Sun, 23 May 2021 23:00:10 +0200
changeset 73775 6bd747b71bd3
parent 73340 0ffcad1f6130
child 73963 59b6f0462086
permissions -rw-r--r--
proper signature export (amending b50f8cc8c08e);
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
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 71692
diff changeset
    26
  def tool(body: => Unit): Unit =
48346
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    27
  {
71687
f17be1db8381 Standard_Thread for isabelle command-line tools;
wenzelm
parents: 71632
diff changeset
    28
    val thread =
71692
f8e52c0152fe clarified names;
wenzelm
parents: 71689
diff changeset
    29
      Isabelle_Thread.fork(name = "command_line", inherit_locals = true) {
71687
f17be1db8381 Standard_Thread for isabelle command-line tools;
wenzelm
parents: 71632
diff changeset
    30
        val rc =
f17be1db8381 Standard_Thread for isabelle command-line tools;
wenzelm
parents: 71632
diff changeset
    31
          try { body; 0 }
f17be1db8381 Standard_Thread for isabelle command-line tools;
wenzelm
parents: 71632
diff changeset
    32
          catch {
f17be1db8381 Standard_Thread for isabelle command-line tools;
wenzelm
parents: 71632
diff changeset
    33
            case exn: Throwable =>
f17be1db8381 Standard_Thread for isabelle command-line tools;
wenzelm
parents: 71632
diff changeset
    34
              Output.error_message(Exn.message(exn) + (if (debug) "\n" + Exn.trace(exn) else ""))
f17be1db8381 Standard_Thread for isabelle command-line tools;
wenzelm
parents: 71632
diff changeset
    35
              Exn.return_code(exn, 2)
f17be1db8381 Standard_Thread for isabelle command-line tools;
wenzelm
parents: 71632
diff changeset
    36
          }
f17be1db8381 Standard_Thread for isabelle command-line tools;
wenzelm
parents: 71632
diff changeset
    37
        sys.exit(rc)
51980
fe16d1128a14 support for more informative crashes;
wenzelm
parents: 48346
diff changeset
    38
      }
71687
f17be1db8381 Standard_Thread for isabelle command-line tools;
wenzelm
parents: 71632
diff changeset
    39
    thread.join
48346
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    40
  }
56631
wenzelm
parents: 55618
diff changeset
    41
71632
c1bc38327bc2 clarified signature;
wenzelm
parents: 71612
diff changeset
    42
  def ML_tool(body: List[String]): String =
c1bc38327bc2 clarified signature;
wenzelm
parents: 71612
diff changeset
    43
    "Command_Line.tool (fn () => (" + body.mkString("; ") + "));"
48346
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    44
}