clarified signature;

suppress dummyT, e.g. from Type_Annotation.print;

tuned proofs;

print type constraints for consts with mixfix syntax;

tuned comments;

obsolete (see 137ea3d464be);

tuned proofs;

tuned whitespace;

more inner-syntax markup;

less instrusive rendering for input buffer (in contrast to 264f043c5da1);

clarified inner-syntax markup;

tuned whitespace;

tuned whitespace;

clarified syntax declarations: keep things together;

tuned;

more inner-syntax markup;

tuned proofs;

more ambitious rendering: highlight active area for mouse hovering without modifier;

tuned proofs;

show_consts_markup is enabled by default;

clarified signature (again, reverting ec1023a5c54c);

clarified signature: more explicit Syntax.print_mode_tabs, depending on print_mode_value (); tuned data structures;

redundant;

tuned signature;

performance tuning: cache markup and extern operations;

minor performance tuning;

minor performance tuning;

backout somewhat pointless 5ea48342e0ae: no need to declare syntax consts for translations (e.g. constraints);

tuned;

tuned;