1.1 --- a/bin/isabelle-process	Thu Feb 28 14:29:54 2013 +0100
     1.2 +++ b/bin/isabelle-process	Thu Feb 28 16:19:08 2013 +0100
     1.3 @@ -96,7 +96,7 @@
     1.4        MLTEXT="$MLTEXT $OPTARG"
     1.5        ;;
     1.6      f)
     1.7 -      MLTEXT="$MLTEXT Session.finish();"
     1.8 +      MLTEXT="$MLTEXT Command_Line.tool0 Session.finish;"
     1.9        ;;
    1.10      m)
    1.11        if [ -z "$MODES" ]; then

     2.1 --- a/src/Pure/System/command_line.ML	Thu Feb 28 14:29:54 2013 +0100
     2.2 +++ b/src/Pure/System/command_line.ML	Thu Feb 28 16:19:08 2013 +0100
     2.3 @@ -7,6 +7,7 @@
     2.4  signature COMMAND_LINE =
     2.5  sig
     2.6    val tool: (unit -> int) -> unit
     2.7 +  val tool0: (unit -> unit) -> unit
     2.8  end;
     2.9  
    2.10  structure Command_Line: COMMAND_LINE =
    2.11 @@ -19,5 +20,7 @@
    2.12          (Output.error_msg (ML_Compiler.exn_message exn); if Exn.is_interrupt exn then 130 else 1);
    2.13      in if rc = 0 then () else exit rc end) ();
    2.14  
    2.15 +fun tool0 body = tool (fn () => (body (); 0));
    2.16 +
    2.17  end;
    2.18