--- a/src/Pure/System/command_line.scala Sat Apr 04 19:30:45 2020 +0200
+++ b/src/Pure/System/command_line.scala Sat Apr 04 20:06:15 2020 +0200
@@ -23,16 +23,20 @@
var debug = false
- def tool(body: => Unit): Nothing =
+ def tool(body: => Unit)
{
- val rc =
- try { body; 0 }
- catch {
- case exn: Throwable =>
- Output.error_message(Exn.message(exn) + (if (debug) "\n" + Exn.trace(exn) else ""))
- Exn.return_code(exn, 2)
+ val thread =
+ Standard_Thread.fork(name = "isabelle", inherit_locals = true) {
+ val rc =
+ try { body; 0 }
+ catch {
+ case exn: Throwable =>
+ Output.error_message(Exn.message(exn) + (if (debug) "\n" + Exn.trace(exn) else ""))
+ Exn.return_code(exn, 2)
+ }
+ sys.exit(rc)
}
- sys.exit(rc)
+ thread.join
}
def ML_tool(body: List[String]): String =