improved scheduling of forked proofs, based on elapsed time estimate (from last run via session log file);

read logs from failed sessions as well; proper output base directory (which is two steps upwards);

recover timing information from old log files; use session timing for queue ordering; pass command timings to ML process (still unused);

suppress timing message in full PIDE protocol -- this is for batch build;

support for build passing timings from Scala to ML;

support for prescient timing information within command transactions;

emit command_timing properties into build log; tuned;

generate Isar proof if Metis appears to be too slow

swap slices so that the last slice is more complete (for minimization)

tuning

ensure all conjecture clauses are in the graph -- to prevent exceptions later

generalize syntax of SPASS proofs

tweaked hack some more

more simplifying constructors

remove needless steps from refutation graph -- these confuse the proof redirection algorithm (and are needless)