enable show_markup by default (approx. double output size);

more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;

explicit show_types takes preferenced over show_markup;

ignore wrapped markup elements in Proof General;

turn constraints into Isabelle_Markup.typing, depending on show_markup options; proper recursion in standard_format;

treat wrapped markup elements as raw markup delimiters;

tuned signature;

tuned proofs;

tuned proofs;

tuned proofs;