Zulip Chat Archive

Stream: general

Topic: Goal window in emacs

Adam Topaz (Sep 01 2020 at 18:43):

A question for the very few people using lean in emacs: are any of you having issues with the goal buffer not updating properly? This seems to happen to me all the time, especially in longer proofs.

Kyle Miller (Sep 01 2020 at 21:25):

I've occasionally had this problem, and I haven't been able to diagnose the issue. Closing and reopening the goal window seems to fix it...

Most recently, I've been having a more wild problem that occasionally my cursor will move to a completely different part of the buffer. I think it has something to do with flycheck windows popping up, resizing a window, and recomputing the cursor position now that it's off-screen, but I haven't been able to diagnose that issue, either.

Adam Topaz (Sep 01 2020 at 21:50):

It's stange... sometimes hitting escape updates the goal buffer, sometimes clicking the buffer with the mouse works, closing/reopening works fairly consistently.

Last updated: Aug 03 2023 at 10:10 UTC