Highlight data should distinguish bindings even in case of state rollback

[david-christiansen]

Currently, when an example contains an error or when the user asks for it, we roll back the elaborator state after an example.

This is generally the right thing, but it has one downside: the unique variable counter gets reset, and later elaborator runs might re-use internal IDs. This can lead to mistaken extra highlights:

There should be some way of preventing this, e.g. by postprocessing the elaborated example to extract the highest ID, then bumping the counter.