merged

enforce rebuild of Isabelle/ML;

clarified signature, following 43323d886ea3;

clarified signature: more direct operation;

clarified signature: more direct Bytes.raw and subsequent UTF-8 default decoding;

clarified signature;

tuned;

unused;

tuned;

clarified signature;

unused;

tuned signature;

simpler theorem

clarified: control verbosity;

enforce rebuild of Isabelle/ML;

more uniform Bytes.read_stream vs. File.read_stream;

clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;

more specialized operations;

notable performance tuning for Library.separated_chunks variants; more direct NoSuchElementException;

tuned;

only consider jobs late if they have ancestors (amending 12901c03b416);

enforce rebuild of Isabelle/ML;

misc tuning: more uniform read_stream vs. read_file;

proper limit for read operation (amending ac4d53bc8f6b);

presumably unused (see also f992769dea97);

remove inactive (e.g., crashed) hosts from scheduling;

tuned;

add timeout to build manager tasks/jobs (e.g. for cluster builds that don't terminate after error on host);