# HG changeset patch
# User wenzelm
# Date 1362064748 -3600
# Node ID 0ce544fbb509cab33642d61dbc9b8933571d13a8
# Parent  337cfc42c9c803cef86ce8987f60b2c8b6c735b2
more robust build error handling, e.g. missing outer syntax commands;

diff -r 337cfc42c9c8 -r 0ce544fbb509 bin/isabelle-process
--- a/bin/isabelle-process	Thu Feb 28 14:29:54 2013 +0100
+++ b/bin/isabelle-process	Thu Feb 28 16:19:08 2013 +0100
@@ -96,7 +96,7 @@
       MLTEXT="$MLTEXT $OPTARG"
       ;;
     f)
-      MLTEXT="$MLTEXT Session.finish();"
+      MLTEXT="$MLTEXT Command_Line.tool0 Session.finish;"
       ;;
     m)
       if [ -z "$MODES" ]; then
diff -r 337cfc42c9c8 -r 0ce544fbb509 src/Pure/System/command_line.ML
--- a/src/Pure/System/command_line.ML	Thu Feb 28 14:29:54 2013 +0100
+++ b/src/Pure/System/command_line.ML	Thu Feb 28 16:19:08 2013 +0100
@@ -7,6 +7,7 @@
 signature COMMAND_LINE =
 sig
   val tool: (unit -> int) -> unit
+  val tool0: (unit -> unit) -> unit
 end;
 
 structure Command_Line: COMMAND_LINE =
@@ -19,5 +20,7 @@
         (Output.error_msg (ML_Compiler.exn_message exn); if Exn.is_interrupt exn then 130 else 1);
     in if rc = 0 then () else exit rc end) ();
 
+fun tool0 body = tool (fn () => (body (); 0));
+
 end;