| author | wenzelm | 
| Wed, 27 Mar 2013 17:58:07 +0100 | |
| changeset 51557 | 4e4b56b7a3a5 | 
| parent 48346 | e2382bede914 | 
| child 51980 | fe16d1128a14 | 
| 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 | |
| 
e2382bede914
more general support for Isabelle/Scala command line tools;
 wenzelm parents: diff
changeset | 24 | def tool(body: => Int): Nothing = | 
| 
e2382bede914
more general support for Isabelle/Scala command line tools;
 wenzelm parents: diff
changeset | 25 |   {
 | 
| 
e2382bede914
more general support for Isabelle/Scala command line tools;
 wenzelm parents: diff
changeset | 26 | val rc = | 
| 
e2382bede914
more general support for Isabelle/Scala command line tools;
 wenzelm parents: diff
changeset | 27 |       try { body }
 | 
| 
e2382bede914
more general support for Isabelle/Scala command line tools;
 wenzelm parents: diff
changeset | 28 |       catch { case exn: Throwable => java.lang.System.err.println(Exn.message(exn)); 2 }
 | 
| 
e2382bede914
more general support for Isabelle/Scala command line tools;
 wenzelm parents: diff
changeset | 29 | sys.exit(rc) | 
| 
e2382bede914
more general support for Isabelle/Scala command line tools;
 wenzelm parents: diff
changeset | 30 | } | 
| 
e2382bede914
more general support for Isabelle/Scala command line tools;
 wenzelm parents: diff
changeset | 31 | } | 
| 
e2382bede914
more general support for Isabelle/Scala command line tools;
 wenzelm parents: diff
changeset | 32 |