# HG changeset patch
# User wenzelm
# Date 1344166941 -7200
# Node ID 181b91e1d1c126fd16016d2bf4d64fdd049b69e4
# Parent  463daacae6c297fd74f49e569e56dcb552702757
prefer general Command_Line.tool wrapper (cf. Scala version);

diff -r 463daacae6c2 -r 181b91e1d1c1 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Sun Aug 05 13:23:54 2012 +0200
+++ b/src/Pure/IsaMakefile	Sun Aug 05 13:42:21 2012 +0200
@@ -189,6 +189,7 @@
   Syntax/syntax_trans.ML				\
   Syntax/term_position.ML				\
   System/build.ML					\
+  System/command_line.ML				\
   System/invoke_scala.ML				\
   System/isabelle_process.ML				\
   System/isabelle_system.ML				\
diff -r 463daacae6c2 -r 181b91e1d1c1 src/Pure/ROOT
--- a/src/Pure/ROOT	Sun Aug 05 13:23:54 2012 +0200
+++ b/src/Pure/ROOT	Sun Aug 05 13:42:21 2012 +0200
@@ -178,6 +178,7 @@
     "Syntax/syntax_trans.ML"
     "Syntax/term_position.ML"
     "System/build.ML"
+    "System/command_line.ML"
     "System/invoke_scala.ML"
     "System/isabelle_process.ML"
     "System/isabelle_system.ML"
diff -r 463daacae6c2 -r 181b91e1d1c1 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sun Aug 05 13:23:54 2012 +0200
+++ b/src/Pure/ROOT.ML	Sun Aug 05 13:42:21 2012 +0200
@@ -268,6 +268,7 @@
 (* Isabelle/Isar system *)
 
 use "System/session.ML";
+use "System/command_line.ML";
 use "System/build.ML";
 use "System/system_channel.ML";
 use "System/isabelle_process.ML";
diff -r 463daacae6c2 -r 181b91e1d1c1 src/Pure/System/build.ML
--- a/src/Pure/System/build.ML	Sun Aug 05 13:23:54 2012 +0200
+++ b/src/Pure/System/build.ML	Sun Aug 05 13:42:21 2012 +0200
@@ -6,7 +6,7 @@
 
 signature BUILD =
 sig
-  val build: string -> unit
+  val build: string -> 'a
 end;
 
 structure Build: BUILD =
@@ -55,8 +55,7 @@
 
 in
 
-fun build args_file = uninterruptible (fn restore_attributes => fn () =>
-  restore_attributes (fn () =>
+fun build args_file = Command_Line.tool (fn () =>
     let
       val (do_output, (options, (verbose, (browser_info, (parent_name,
           (name, theories)))))) =
@@ -83,11 +82,8 @@
             |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads"));
 
       val _ = Session.finish ();
-      val _ = if do_output then () else quit ();
-    in () end) ()) ()
-  handle exn =>
-    (Output.error_msg (ML_Compiler.exn_message exn);
-     if Exn.is_interrupt exn then exit 130 else exit 1);
+      val _ = if do_output then Secure.commit () else ();
+    in 0 end);
 
 end;
 
diff -r 463daacae6c2 -r 181b91e1d1c1 src/Pure/System/command_line.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/command_line.ML	Sun Aug 05 13:42:21 2012 +0200
@@ -0,0 +1,23 @@
+(*  Title:      Pure/System/command_line.ML
+    Author:     Makarius
+
+Support for Isabelle/ML command line tools.
+*)
+
+signature COMMAND_LINE =
+sig
+  val tool: (unit -> int) -> 'a
+end;
+
+structure Command_Line: COMMAND_LINE =
+struct
+
+fun tool body =
+  uninterruptible (fn restore_attributes => fn () =>
+    let val rc =
+      restore_attributes body () handle exn =>
+        (Output.error_msg (ML_Compiler.exn_message exn); if Exn.is_interrupt exn then 130 else 1);
+    in exit rc; raise Fail "ERROR" end) ();
+
+end;
+