Pause emacs info

Stream: new members

[Felipe]

Is there a way to pause/freeze the *Lean Goal* buffer so it doesn't update as point is moved around? I want to be able to switch to a different buffer or part of the buffer while keeping the goal open to think about how to make progress

[Kevin Buzzard]

Click on the "pause" icon. Edit: Oh sorry -- this is an emacs question? I don't know. In general VS Code has far more bells and whistles than emacs.

[Felipe]

Thanks. Feared as much! Thankfully Emacs makes it easy to hack such things in :smile: https://github.com/leanprover/lean4-mode/issues/22