clarified output;

support for global registry;

clarified loading of symbols: permissive entries in $ISABELLE_SYMBOLS require explicit "?";

slightly less technical formulation of very specific type class

weakened dependency

explicit type class for discrete linordered semidoms

proper dummy timing entries;

use only finished sessions in timing data;

tuned;

performance tuning for build schedule: explicit schedule generation, without mixing heuristics;

performance tuning for build schedule: faster stopping;

performance tuning for timing heuristic: pre-calculate graph operations;

move timing data into scheduler for more efficient heuristics (e.g., with pre-calculated values);

clarified signature: emphasize mutable instance;

clarified signature: more operations;