search

Julian / lean.nvim

Neovim support for the Lean theorem prover
MIT License
278 stars 27 forks source link

Closing the infoview buffer with :q! causes errors #346

Closed stephen-huan closed 3 months ago

stephen-huan commented 3 months ago

If I close the infoview window manually with :q!, it errors with

Error executing vim.schedule lua callback: ...mPackages/start/plenary.nvim/lua/plenary/async/async.lua:18: The coroutine failed with this message: ...k/myNeovimPackages/start/lean.nv
im/lua/lean/infoview.lua:680: Invalid window id: 1002
stack traceback:
        [C]: in function 'error'
        ...mPackages/start/plenary.nvim/lua/plenary/async/async.lua:18: in function 'callback_or_next'
        ...mPackages/start/plenary.nvim/lua/plenary/async/async.lua:45: in function 'handler'
        ...wrapped-0.10.0/share/nvim/runtime/lua/vim/lsp/client.lua:685: in function ''
        vim/_editor.lua: in function <vim/_editor.lua:0>
Press ENTER or type command to continue

and these errors happen periodically afterwards when I move my cursor as well. Since these errors don't happen with :q, I thought it may be a difference in the autocmd trigger order. Below is what autocmds trigger with :q

18:56:46 - Started autocmd log (2024-07-17)
18:56:46 - CursorHold
18:56:49 - QuitPre
18:56:49 - BufLeave
18:56:49 - WinLeave
18:56:49 - WinClosed
18:56:49 - BufWinLeave
18:56:49 - BufHidden
18:56:49 - WinEnter
18:56:49 - BufEnter
18:56:49 - CursorMoved
18:56:49 - User
18:56:50 - CursorHold
18:56:52 - Stopped autocmd log (2024-07-17)

and with :q!. Note that unlike with :q, WinClosed activates immediately and then again slightly later.

18:57:07 - Started autocmd log (2024-07-17)
18:57:07 - CursorHold
18:57:08 - WinClosed
18:57:08 - BufWinLeave
18:57:08 - BufHidden
18:57:10 - QuitPre
18:57:10 - BufLeave
18:57:10 - WinLeave
18:57:10 - WinClosed
18:57:10 - BufWinLeave
18:57:10 - BufUnload
18:57:10 - WinEnter
18:57:10 - BufEnter
18:57:10 - CursorMoved
18:57:11 - User
18:57:12 - CursorHold
18:57:13 - Stopped autocmd log (2024-07-17)

Related to https://github.com/Julian/lean.nvim/issues/20 but the error is slightly different: window id vs buffer id.

stephen-huan commented 3 months ago

Indirectly addressed by https://github.com/Julian/lean.nvim/issues/43, which I would love to see finally merged as well.

Julian commented 3 months ago

I'd somewhat say "don't do that" :) as using :q! on a buffer with no modifications is pointless, but nonetheless given this wasn't impossible to work around I've pushed a fix. Give it a shot and feel free to let me know if you notice anything else!

stephen-huan commented 3 months ago

Give it a shot and feel free to let me know if you notice anything else!

It works, thanks for the fix!

I'd somewhat say "don't do that" :) as using :q! on a buffer with no modifications is pointless, but nonetheless given this wasn't impossible to work around I've pushed a fix.

I agree, the reason is I have <ctrl-q> bound to :q! so I use that shortcut reflexively to close any window. I've been using https://github.com/Julian/lean.nvim/issues/43#issuecomment-2234820480 so I don't need to do this manually anymore, thankfully. I raised the issue because, well, the dual to ":q! is the same as :q so don't do :q!" is ":q! is the same as :q so both should work" :p.