equal
deleted
inserted
replaced
19 chunk :: chunks(rest.tail) |
19 chunk :: chunks(rest.tail) |
20 } |
20 } |
21 def unapplySeq(list: List[String]): Option[List[List[String]]] = Some(chunks(list)) |
21 def unapplySeq(list: List[String]): Option[List[List[String]]] = Some(chunks(list)) |
22 } |
22 } |
23 |
23 |
24 var debug = false |
|
25 |
|
26 def tool(body: => Unit): Unit = |
24 def tool(body: => Unit): Unit = |
27 { |
25 { |
28 val thread = |
26 val thread = |
29 Isabelle_Thread.fork(name = "command_line", inherit_locals = true) { |
27 Isabelle_Thread.fork(name = "command_line", inherit_locals = true) { |
30 val rc = |
28 val rc = |
31 try { body; 0 } |
29 try { body; 0 } |
32 catch { |
30 catch { |
33 case exn: Throwable => |
31 case exn: Throwable => |
34 Output.error_message(Exn.message(exn) + (if (debug) "\n" + Exn.trace(exn) else "")) |
32 Output.error_message(Exn.print(exn)) |
35 Exn.return_code(exn, 2) |
33 Exn.return_code(exn, 2) |
36 } |
34 } |
37 sys.exit(rc) |
35 sys.exit(rc) |
38 } |
36 } |
39 thread.join |
37 thread.join |