VSCode extension : 'Toggle updating' hides infoview

Stream: general

[Peter Nelson]

I don't know if this is just a problem with my VSCode or something from an update, but suddenly the option 'Lean4 Infoview : toggle updating' minimizes the tactic state. It can be shown again by clicking on the little arrow, but it disappears again on the next toggle.

My whole workflow relies on being able to frequently see a frozen version of the tactic state rather than have it jump around while I'm typing - I can't be the only one!

Is anyone else having this issue or aware of a solution?

[Marc Huisinga]

Looks like this was introduced by the vscode-lean4 release from a couple of hours ago. Thanks for reporting this, I'll look into fixing this immediately.

[Marc Huisinga]

0.0.138 is in the process of being released and includes a fix.

[Peter Nelson]

Amazing - thanks!