# HG changeset patch # User wenzelm # Date 1586023575 -7200 # Node ID f17be1db8381a0043fb2d746e973a40bbbf870f0 # Parent eb44cf7ae9267b25733c848221758c0961661ed9 Standard_Thread for isabelle command-line tools; diff -r eb44cf7ae926 -r f17be1db8381 src/Pure/System/command_line.scala --- 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 =