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;