Enable display of variable types (low priority)

[david-a-wheeler]

I'd love to expand controls over what explorer tab can show, in particular variable types ($f).

Currently there's a single "Assertion type" which can be "Axioms", "Theorems", or "All" (which really just means axioms & theorems). It'd be awesome to also be able to show "Variable types" (aka $f aka "floating" assertions. I suspect it'd be better to have a checkbox (on/off) for each of axioms, theorems, and variable types. This would also imply that variable type labels could be displayed and clicked on, e.g., this set.mm statement:

 $( Let variable ` ph ` be a wff. $)
  wph $f wff ph $.

Would be displayed in the explorer as something like (the text after > is on open):

Variable Type wph > [ Let variable ` ph ` be a wff. ]
wff ph

Clicking on the wph would produce a tab showing its description followed by Typecode VariableName, e.g.,:

Variable Type wph
Let variable ` ph ` be a wff.

wff ph

These would also be clickable in other tables where syntax is shown.

The idea is that, since it already supports showing syntax tables, it'd make more sense to go down to declaring the types of each symbol. This would eliminate the mystery of "how does it determine the type of ph ?" and similar.