equal
deleted
inserted
replaced
|
1 /* Title: Pure/System/command_line.scala |
|
2 Author: Makarius |
|
3 |
|
4 Support for Isabelle/Scala command line tools. |
|
5 */ |
|
6 |
|
7 package isabelle |
|
8 |
|
9 |
|
10 object Command_Line |
|
11 { |
|
12 object Chunks |
|
13 { |
|
14 private def chunks(list: List[String]): List[List[String]] = |
|
15 list.indexWhere(_ == "\n") match { |
|
16 case -1 => List(list) |
|
17 case i => |
|
18 val (chunk, rest) = list.splitAt(i) |
|
19 chunk :: chunks(rest.tail) |
|
20 } |
|
21 def unapplySeq(list: List[String]): Option[List[List[String]]] = Some(chunks(list)) |
|
22 } |
|
23 |
|
24 def tool(body: => Int): Nothing = |
|
25 { |
|
26 val rc = |
|
27 try { body } |
|
28 catch { case exn: Throwable => java.lang.System.err.println(Exn.message(exn)); 2 } |
|
29 sys.exit(rc) |
|
30 } |
|
31 } |
|
32 |