more Java heap space for the sake of Isabelle/AFP cluster build stability, but this is better changed elsewhere; enforce rebuild of Isabelle/ML;

merged

build_progress with percentage;

clarified signature: prefer static percentage;

more informative Progress.Nodes_Status;

more informative Command_Span.Theory_Span;

tuned;

more accurate theory timing, based on sum of command timings; remove obsolete protocol message;

support for detailed build progress;

proper symbolic_path for nodes_domain;

tuned;

tuned signature;

clarified signature;

more thorough Command.State.exit vs. Command.init_state: avoid loss of information in Document.State.end_theory (notably Command_Timings);

clarified internal protocol: accept is_theory, reject add_markup;

more concise storage of Command.State: omit pointless status: List[Markup];

avoid shortcuts based on potentially expensive equality test;

clarified signature: more explicit type Progress.Nodes_Status;

prefer robust Timing_Properties.get;

unused (see also 88dfbc382a3d);

more accurate markup for command timing, notably for theory pseudo-command in batch-build, but also for accidental occurrences of command keywords (e.g. in command definition);

more detailed Command_Timings: count actual commands from theory body individually;

basic setup for build progress with nodes_status;

clarified signature;