| author | wenzelm |
| Fri, 07 Apr 2017 18:26:30 +0200 | |
| changeset 65430 | 4433d189a77d |
| 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:
56671
diff
changeset
|
33 |
Output.error_message(Exn.message(exn)) |
|
56669
f42717b5dc84
clarified message and return code, in accordance to ML version;
wenzelm
parents:
56631
diff
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 |