src/Pure/System/command_line.scala
author wenzelm
Mon, 26 Jul 2021 13:12:22 +0200
changeset 74068 62e4ec8cff38
parent 73963 59b6f0462086
child 74140 8a5e02ef975c
permissions -rw-r--r--
clarified signature;
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
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 71692
diff changeset
    24
  def tool(body: => Unit): Unit =
48346
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    25
  {
71687
f17be1db8381 Standard_Thread for isabelle command-line tools;
wenzelm
parents: 71632
diff changeset
    26
    val thread =
71692
f8e52c0152fe clarified names;
wenzelm
parents: 71689
diff changeset
    27
      Isabelle_Thread.fork(name = "command_line", inherit_locals = true) {
71687
f17be1db8381 Standard_Thread for isabelle command-line tools;
wenzelm
parents: 71632
diff changeset
    28
        val rc =
f17be1db8381 Standard_Thread for isabelle command-line tools;
wenzelm
parents: 71632
diff changeset
    29
          try { body; 0 }
f17be1db8381 Standard_Thread for isabelle command-line tools;
wenzelm
parents: 71632
diff changeset
    30
          catch {
f17be1db8381 Standard_Thread for isabelle command-line tools;
wenzelm
parents: 71632
diff changeset
    31
            case exn: Throwable =>
73963
59b6f0462086 clarified modules;
wenzelm
parents: 73340
diff changeset
    32
              Output.error_message(Exn.print(exn))
74068
62e4ec8cff38 clarified signature;
wenzelm
parents: 73963
diff changeset
    33
              Exn.failure_rc(exn)
71687
f17be1db8381 Standard_Thread for isabelle command-line tools;
wenzelm
parents: 71632
diff changeset
    34
          }
f17be1db8381 Standard_Thread for isabelle command-line tools;
wenzelm
parents: 71632
diff changeset
    35
        sys.exit(rc)
51980
fe16d1128a14 support for more informative crashes;
wenzelm
parents: 48346
diff changeset
    36
      }
71687
f17be1db8381 Standard_Thread for isabelle command-line tools;
wenzelm
parents: 71632
diff changeset
    37
    thread.join
48346
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    38
  }
56631
wenzelm
parents: 55618
diff changeset
    39
71632
c1bc38327bc2 clarified signature;
wenzelm
parents: 71612
diff changeset
    40
  def ML_tool(body: List[String]): String =
c1bc38327bc2 clarified signature;
wenzelm
parents: 71612
diff changeset
    41
    "Command_Line.tool (fn () => (" + body.mkString("; ") + "));"
48346
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    42
}