Implement goal state diff-ing

[Julian]

Given a sequence of tactics, load the goal state text at the end of each tactic into the quickfix list and allow a sequential (text) vimdiff of the state from one to the next.

[Julian]

Though not quite as I wrote it out here X years ago (wow, years!) -- @jcommelin pointed out that VSCode has this! At least in Lean 4. Somehow I've never noticed, but if you move around a proof script, VSCode will highlight what changed in the goal state.

We should find whatever code is responsible for doing that and reproduce it here -- hopefully it's mostly server side rather than manually diffing the state...