Add an optional executed code overlay

[KacperFKorban]

Description and Motivation

This PR adds an overlay that appears over executed (and pending) HOL4 code in the current working editor. The feature is hidden by an option and is bu default set to off.

This solves one of my main problems when reading HOL4 code:

1. I start a goal
2. I execute some tactics
3. I jump around the editor, to inspect some definitions or just look at some code in a different editor or ...
4. I come back to the HOL4 editor or I cannot figure out what was the state of my proof.

Demo:

Kooha-2025-10-03-13-23-41.webm

Discussion

It is not clear to me what should be the expected result after removing an "executed" piece of code. Should the we go back in the proof before that line was executed? AFAIK this can only be done in a "goal" state.

Should there be a better visual indication of the order of executed selections? This could either be done with a gradient or minimally, an indication of the last executed code selection. This might be useful for people that don't necessarily follow a linear order, when developing a proof.

Keeping the list of executed actions opens a possibility of adding a "Send since last selection" command. Would that be useful? (I think that it makes sense for tactics)

[digama0]

I have some plans here in the direction of keeping information on all intermediate states and allowing you to edit anywhere, similar to how lean works, but I think this feature is useful anyway for working with the current system without getting lost, so I think it will be good to have as an option regardless.