Have matching begin-end keywords light each other up

[david-christiansen]

Hovering the "end" keyword of a mutual block should cause the "mutual" keyword to also light up in HTML output. This goes for other blocks terminated by end as well, like section - this sends a useful signal to new users, as much Lean style relies on the presence of things like IDE breadcrumbs that aren't present in examples in documents.