Goal window in emacs

Stream: general

[Adam Topaz]

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]

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]

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