| author | wenzelm | 
| Sat, 17 Feb 2018 19:37:18 +0100 | |
| changeset 67647 | 27f3dceb5a70 | 
| parent 56782 | 433cf57550fa | 
| child 68806 | 4597812d5182 | 
| 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 | ||
| 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 | 30 |       catch {
 | 
| 31 | case exn: Throwable => | |
| 32 | if (debug) exn.printStackTrace | |
| 56782 
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
 wenzelm parents: 
56671diff
changeset | 33 | Output.error_message(Exn.message(exn)) | 
| 56669 
f42717b5dc84
clarified message and return code, in accordance to ML version;
 wenzelm parents: 
56631diff
changeset | 34 | Exn.return_code(exn, 2) | 
| 51980 | 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 | 38 | |
| 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 |