proper PIDE positions;

avoid race condition wrt. ISABELLE_TMP, which is removed in Bash.cleanup() before Bash.result(progress_stdout);

clarified "consolidation" vs. "presentation";

tuned signature;

merged

tuned;

more thorough checks for theory name consistency (for extend, not just merge);

more uniform output (cf. 450cefec7c11);

removed duplicates

added lemmas

tuned headers;

move FuncSet back to HOL-Library (amending 493b818e8e10)

merged

cleaning up sorted

merged

support for dynamic document output while editing;

adjust position according to offset of command/exec id;

tuned signature (see Command.eval_state);

export generated document.tex, unless explicit document=false;

more general presentation hook, with document preparation as application;

clarified signature: more explicit type "context" with full options;

more explicit type Thy_Output.segment;

clarified signature; more operations;

more sorted cleaning

cleaning up sorted

merged

more uniform types vs. consts;

more concise information;