| author | blanchet | 
| Fri, 14 Feb 2014 07:53:45 +0100 | |
| changeset 55463 | 942c2153b5b4 | 
| parent 51980 | fe16d1128a14 | 
| child 55618 | 995162143ef4 | 
| 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 | |
| 33 | java.lang.System.err.println(Exn.message(exn)) | |
| 34 | 2 | |
| 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 | } | 
| 
e2382bede914
more general support for Isabelle/Scala command line tools;
 wenzelm parents: diff
changeset | 38 | } | 
| 
e2382bede914
more general support for Isabelle/Scala command line tools;
 wenzelm parents: diff
changeset | 39 |