more robust build error handling, e.g. missing outer syntax commands;

--- 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

--- 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;