src/Pure/System/command_line.scala
author wenzelm
Fri, 01 Apr 2022 17:06:10 +0200
changeset 75393 87ebf5a50283
parent 74306 a117c076aa22
permissions -rw-r--r--
clarified formatting, for the sake of scala3;
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
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74306
diff changeset
    10
object Command_Line {
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74306
diff changeset
    11
  object Chunks {
48346
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    12
    private def chunks(list: List[String]): List[List[String]] =
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    13
      list.indexWhere(_ == "\n") match {
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    14
        case -1 => List(list)
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    15
        case i =>
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    16
          val (chunk, rest) = list.splitAt(i)
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    17
          chunk :: chunks(rest.tail)
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    18
      }
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    19
    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
    20
  }
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    21
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74306
diff changeset
    22
  def tool(body: => Unit): Unit = {
71687
f17be1db8381 Standard_Thread for isabelle command-line tools;
wenzelm
parents: 71632
diff changeset
    23
    val thread =
71692
f8e52c0152fe clarified names;
wenzelm
parents: 71689
diff changeset
    24
      Isabelle_Thread.fork(name = "command_line", inherit_locals = true) {
71687
f17be1db8381 Standard_Thread for isabelle command-line tools;
wenzelm
parents: 71632
diff changeset
    25
        val rc =
74306
a117c076aa22 clarified signature;
wenzelm
parents: 74140
diff changeset
    26
          try { body; Process_Result.RC.ok }
71687
f17be1db8381 Standard_Thread for isabelle command-line tools;
wenzelm
parents: 71632
diff changeset
    27
          catch {
f17be1db8381 Standard_Thread for isabelle command-line tools;
wenzelm
parents: 71632
diff changeset
    28
            case exn: Throwable =>
73963
59b6f0462086 clarified modules;
wenzelm
parents: 73340
diff changeset
    29
              Output.error_message(Exn.print(exn))
74068
62e4ec8cff38 clarified signature;
wenzelm
parents: 73963
diff changeset
    30
              Exn.failure_rc(exn)
71687
f17be1db8381 Standard_Thread for isabelle command-line tools;
wenzelm
parents: 71632
diff changeset
    31
          }
f17be1db8381 Standard_Thread for isabelle command-line tools;
wenzelm
parents: 71632
diff changeset
    32
        sys.exit(rc)
51980
fe16d1128a14 support for more informative crashes;
wenzelm
parents: 48346
diff changeset
    33
      }
74140
8a5e02ef975c clarified signature;
wenzelm
parents: 74068
diff changeset
    34
    thread.join()
48346
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    35
  }
56631
wenzelm
parents: 55618
diff changeset
    36
71632
c1bc38327bc2 clarified signature;
wenzelm
parents: 71612
diff changeset
    37
  def ML_tool(body: List[String]): String =
c1bc38327bc2 clarified signature;
wenzelm
parents: 71612
diff changeset
    38
    "Command_Line.tool (fn () => (" + body.mkString("; ") + "));"
48346
e2382bede914 more general support for Isabelle/Scala command line tools;
wenzelm
parents:
diff changeset
    39
}