author | wenzelm |
Thu, 19 Jul 2012 12:05:54 +0200 | |
changeset 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 |