annotate binders, light doc styling

[ammkrn]

• gives a different class to term v. def and axiom v. theorem,
• changes the pretty printer implementation so that it annotates variables in binders with their sort info
• sort names are now an intra-doc links
• applies some basic styling so you get an idea of how any given palette will compose. The colors are based on this palette

[digama0]

Thanks. I added the dark style as well. I removed the :link selectors because I found it confusing that "wff" was red and "nat" was orange until I realized that I had clicked on one and not the other. The colors can be better put to use tracking semantic info.

[ammkrn]

I removed the :link selectors because I found it confusing that "wff" was red and "nat" was orange until I realized that I had clicked on one and not the other.

I just noticed it, but another minor tweak (actually I think this is what caused the thing you saw too) that needs to be made is that declarations rendered by thm_doc for subpages don't differentiate between the kinds of term/theorem, so the sub-pages for axioms show axioms with the "thm" class.

[digama0]

that's true, probably also in conv proof steps it needs to use def (actually it should always be def)