src/Pure/System/command_line.ML
2013-02-28 ago more robust build error handling, e.g. missing outer syntax commands;
2012-08-08 ago more casual exit back to ML toplevel, to accomodate commit in SML/NJ which continues at the saved point;
2012-08-05 ago prefer general Command_Line.tool wrapper (cf. Scala version);