author | wenzelm |
Thu, 28 Feb 2013 16:19:08 +0100 | |
changeset 52449 | 0ce544fbb509 |
parent 49746 | a45ba78abcc1 |
child 53823 | f4871fe80410 |
permissions | -rw-r--r-- |
wenzelm@49696 | 1 |
(* Title: Pure/System/command_line.ML |
wenzelm@49696 | 2 |
Author: Makarius |
wenzelm@49696 | 3 |
|
wenzelm@49696 | 4 |
Support for Isabelle/ML command line tools. |
wenzelm@49696 | 5 |
*) |
wenzelm@49696 | 6 |
|
wenzelm@49696 | 7 |
signature COMMAND_LINE = |
wenzelm@49696 | 8 |
sig |
wenzelm@49746 | 9 |
val tool: (unit -> int) -> unit |
wenzelm@52449 | 10 |
val tool0: (unit -> unit) -> unit |
wenzelm@49696 | 11 |
end; |
wenzelm@49696 | 12 |
|
wenzelm@49696 | 13 |
structure Command_Line: COMMAND_LINE = |
wenzelm@49696 | 14 |
struct |
wenzelm@49696 | 15 |
|
wenzelm@49696 | 16 |
fun tool body = |
wenzelm@49696 | 17 |
uninterruptible (fn restore_attributes => fn () => |
wenzelm@49696 | 18 |
let val rc = |
wenzelm@49696 | 19 |
restore_attributes body () handle exn => |
wenzelm@49696 | 20 |
(Output.error_msg (ML_Compiler.exn_message exn); if Exn.is_interrupt exn then 130 else 1); |
wenzelm@49746 | 21 |
in if rc = 0 then () else exit rc end) (); |
wenzelm@49696 | 22 |
|
wenzelm@52449 | 23 |
fun tool0 body = tool (fn () => (body (); 0)); |
wenzelm@52449 | 24 |
|
wenzelm@49696 | 25 |
end; |
wenzelm@49696 | 26 |