back to cumulative treatment of command status, which is important for total accounting (amending 8201790fdeb9);

tuned;

redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands); more explicit ML_Compiler.flags;

clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;