Highlight changes in goal state

[Kha]

tl;dr: https://twitter.com/famontesi/status/1557346899610443782

We already have both the state before and after a tactic in the info tree, we should use them at the same time! A full diff is probably too noisy since the old state is usually less interesting than the new one, as long as you can see where it changed at all. We could probably do this by diffing the TaggedTexts, introducing a new kind of MsgEmbed. The Coq implementation is documented at https://coq.inria.fr/distrib/current/refman/proofs/writing-proofs/proof-mode.html#how-diffs-are-calculated.

[EdAyers]

I am keen to work on this

[EdAyers]

I can think of two ways of implementing this:

1. VSCode's goal view component intercepts rendering of tagged text and highlights subexpressions that have changed since the last render. React provides some mechanisms for remembering what the last state was, so this could be done entirely on the client.
2. Lean computes the diffs in goal state, each fileworker remembers the last goal that was requested and alongside the InteractiveGoal object, we also pass an InteractiveGoalDiff, which in turn includes an ExprDiff which the vscode extension can then render.

[Kha]

I don't think it should depend on the navigation history but always, deterministically provide the diff between the selected tactic's pre and post state - which would be convenient because that's exactly the information we already have in every TacticInfo. I didn't check Coq's behavior myself, but from the description I'm assuming they do this as well.