Subverso Highlighting

[jcreedcmu]

Use subverso for highlighting instead of highlightjs.

To use:

cd md
make 
make deploy
make serve
# browse to localhost:8000
# for example, navigate to Maths > Sets > 11. Proving Set Equalites
# and hover over `subset_antisymm_iff`

Known problems: some of the highlight regions are wrong, still looking into it.

[klavins]

So far this looks fantastic.

[klavins]

I tested the PR and fixed a few issues that make it so that the highlight are aligned (at least in the cases I could find). Changes are on the subverso-fixes branch.

Do you think we can get to this to the point that we have proof states?

Specific changes:

• index.html — added the missing subverso-highlight.js script tag (in both source and dist)
• slider.js — moved the subverso highlighting call from dist-only to the source file so deploy doesn't overwrite it
• subverso-highlight.js — replaced offset-based token matching with sequential string matching + word boundaries, fixing misaligned tooltips

[jcreedcmu]

Nice! I'm actually wondering whether it might be feasible to swing you over to using https://github.com/leanprover/verso-slides , which didn't exist when we first talked --- it definitely does have full proof state visualization.

[klavins]

Ok, I'll take a look.