1.1 --- a/src/Pure/IsaMakefile	Sun Aug 05 13:23:54 2012 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Sun Aug 05 13:42:21 2012 +0200
     1.3 @@ -189,6 +189,7 @@
     1.4    Syntax/syntax_trans.ML				\
     1.5    Syntax/term_position.ML				\
     1.6    System/build.ML					\
     1.7 +  System/command_line.ML				\
     1.8    System/invoke_scala.ML				\
     1.9    System/isabelle_process.ML				\
    1.10    System/isabelle_system.ML				\

     2.1 --- a/src/Pure/ROOT	Sun Aug 05 13:23:54 2012 +0200
     2.2 +++ b/src/Pure/ROOT	Sun Aug 05 13:42:21 2012 +0200
     2.3 @@ -178,6 +178,7 @@
     2.4      "Syntax/syntax_trans.ML"
     2.5      "Syntax/term_position.ML"
     2.6      "System/build.ML"
     2.7 +    "System/command_line.ML"
     2.8      "System/invoke_scala.ML"
     2.9      "System/isabelle_process.ML"
    2.10      "System/isabelle_system.ML"

     3.1 --- a/src/Pure/ROOT.ML	Sun Aug 05 13:23:54 2012 +0200
     3.2 +++ b/src/Pure/ROOT.ML	Sun Aug 05 13:42:21 2012 +0200
     3.3 @@ -268,6 +268,7 @@
     3.4  (* Isabelle/Isar system *)
     3.5  
     3.6  use "System/session.ML";
     3.7 +use "System/command_line.ML";
     3.8  use "System/build.ML";
     3.9  use "System/system_channel.ML";
    3.10  use "System/isabelle_process.ML";

     4.1 --- a/src/Pure/System/build.ML	Sun Aug 05 13:23:54 2012 +0200
     4.2 +++ b/src/Pure/System/build.ML	Sun Aug 05 13:42:21 2012 +0200
     4.3 @@ -6,7 +6,7 @@
     4.4  
     4.5  signature BUILD =
     4.6  sig
     4.7 -  val build: string -> unit
     4.8 +  val build: string -> 'a
     4.9  end;
    4.10  
    4.11  structure Build: BUILD =
    4.12 @@ -55,8 +55,7 @@
    4.13  
    4.14  in
    4.15  
    4.16 -fun build args_file = uninterruptible (fn restore_attributes => fn () =>
    4.17 -  restore_attributes (fn () =>
    4.18 +fun build args_file = Command_Line.tool (fn () =>
    4.19      let
    4.20        val (do_output, (options, (verbose, (browser_info, (parent_name,
    4.21            (name, theories)))))) =
    4.22 @@ -83,11 +82,8 @@
    4.23              |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads"));
    4.24  
    4.25        val _ = Session.finish ();
    4.26 -      val _ = if do_output then () else quit ();
    4.27 -    in () end) ()) ()
    4.28 -  handle exn =>
    4.29 -    (Output.error_msg (ML_Compiler.exn_message exn);
    4.30 -     if Exn.is_interrupt exn then exit 130 else exit 1);
    4.31 +      val _ = if do_output then Secure.commit () else ();
    4.32 +    in 0 end);
    4.33  
    4.34  end;
    4.35  

     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Pure/System/command_line.ML	Sun Aug 05 13:42:21 2012 +0200
     5.3 @@ -0,0 +1,23 @@
     5.4 +(*  Title:      Pure/System/command_line.ML
     5.5 +    Author:     Makarius
     5.6 +
     5.7 +Support for Isabelle/ML command line tools.
     5.8 +*)
     5.9 +
    5.10 +signature COMMAND_LINE =
    5.11 +sig
    5.12 +  val tool: (unit -> int) -> 'a
    5.13 +end;
    5.14 +
    5.15 +structure Command_Line: COMMAND_LINE =
    5.16 +struct
    5.17 +
    5.18 +fun tool body =
    5.19 +  uninterruptible (fn restore_attributes => fn () =>
    5.20 +    let val rc =
    5.21 +      restore_attributes body () handle exn =>
    5.22 +        (Output.error_msg (ML_Compiler.exn_message exn); if Exn.is_interrupt exn then 130 else 1);
    5.23 +    in exit rc; raise Fail "ERROR" end) ();
    5.24 +
    5.25 +end;
    5.26 +