more markup (without rendering): class, type constructor, term constant --- similar to free, bound, etc.;

tuned: more robust wrt. changes the Markup space;

tuned: prefer explicit names of inferred types;

more accurate HTML markup: suppress text_color that has_syntax (amending b57996a0688c);

clarified signature;

tuned;

clarified signature;

clarified term positions and markup: syntax = true means this is via concrete syntax; clarified text color rendering;

tuned signature: more operations;

tuned;

clarified signature: more explicit operations;

tuned;

tuned whitespace;

clarified signature and caching;