tuned signature: expose internal limits for testing or add-on implementations;

tuned;

tuned;

tuned;

tuned;

clarified signature;

prefer official UTF-8 decoding (in contrast to 2541de190d92): this is also more efficient (factor 10-20);

tuned;

unused (see also c2f176a38448);

more robust message header: prefer explicit props_length/props_chunks over odd YXML.embed_controls;

tuned signature: more operations;

tuned comments;

tuned whitespace;

use ansi colored diffs;

add diffs to build manager;

clarified: components vs. extra components;

compress reports;

clarified build report;

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;