| author | wenzelm | 
| Sat, 05 Jun 2021 20:20:25 +0200 | |
| changeset 73814 | c8b4a4f69068 | 
| parent 73340 | 0ffcad1f6130 | 
| child 73963 | 59b6f0462086 | 
| permissions | -rw-r--r-- | 
| 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 | 24 | var debug = false | 
| 25 | ||
| 73340 | 26 | def tool(body: => Unit): Unit = | 
| 48346 
e2382bede914
more general support for Isabelle/Scala command line tools;
 wenzelm parents: diff
changeset | 27 |   {
 | 
| 71687 | 28 | val thread = | 
| 71692 | 29 |       Isabelle_Thread.fork(name = "command_line", inherit_locals = true) {
 | 
| 71687 | 30 | val rc = | 
| 31 |           try { body; 0 }
 | |
| 32 |           catch {
 | |
| 33 | case exn: Throwable => | |
| 34 | Output.error_message(Exn.message(exn) + (if (debug) "\n" + Exn.trace(exn) else "")) | |
| 35 | Exn.return_code(exn, 2) | |
| 36 | } | |
| 37 | sys.exit(rc) | |
| 51980 | 38 | } | 
| 71687 | 39 | thread.join | 
| 48346 
e2382bede914
more general support for Isabelle/Scala command line tools;
 wenzelm parents: diff
changeset | 40 | } | 
| 56631 | 41 | |
| 71632 | 42 | def ML_tool(body: List[String]): String = | 
| 43 |     "Command_Line.tool (fn () => (" + body.mkString("; ") + "));"
 | |
| 48346 
e2382bede914
more general support for Isabelle/Scala command line tools;
 wenzelm parents: diff
changeset | 44 | } |