I've made a fair amount of progress towards my goal of nicer HTML display of theorems. It's still rough and there's more I want to do, but I figured now is as good a checkpoint as any.
It's relatively easy to build from source, but I've also put files up on static serving:
Hovering over a proof step highlights the "arguments" of the step. Clicking on it brings up an info card. There's lots more that I want to put on the card (the statement of the theorem, the explicit substitution of the variables), but the fact that it displays the result line is a start.
Also note that the translation from Metamath is cruder than I'd like - it puts a label on every line whether needed or not, it makes lines for every step even if it could be inlined without parentheses.
Even though it's not quite my vision, I thought people on this list would like to see where I'm going with this.