Zulip Chat Archive

Stream: new members

Topic: How to see entire "Processing file" message string?


mars0i (Sep 07 2024 at 18:54):

In neovim, if Lean decides that it needs to run a long process to build some library that I've imported, I get the "Processing file..." message, and there's also a message (in red in my configuration) that floats at the right top line of my source file. However, this message is very long, and I can't see the whole string unless I make my window very large and my font very small.

(Sometimes hidden right side of the message is important, for example "failed: stderr: ....".)

Is there some way to see the whole message in neovim, or is there a log file somewhere that contains the message? (I'm on MacOS, but if you know the answer for Linux or Windows, I can look for the corresponding file on my system.)

Julian Berman (Sep 07 2024 at 18:55):

:lua vim.diagnostic.open_float() is the most basic way to see the whole message. It takes various options if you want to customize what you see.

Julian Berman (Sep 07 2024 at 18:56):

I have it bound to <leader>K with a few tweaks:

vim.keymap.set('n', '<leader>K', function()
    vim.diagnostic.open_float{ scope = "line", header = '', focus = false }
end, { desc = 'show information about line diagnostics in a float' })

mars0i (Sep 07 2024 at 18:59):

Ah, thank you @Julian Berman. I'm not going to say it's life-changing--but relative to this narrow context, it kind of is.

mars0i (Sep 07 2024 at 19:19):

Weird--:lua vim.diagnostic.open_float() stopped working. Investigating.

mars0i (Sep 07 2024 at 19:20):

Never mind. It works when cursor is on the line with the float.

Julian Berman (Sep 07 2024 at 19:29):

That's what scope = 'line' controls in my example above (which is also the default if you provide nothing). I like that behavior and typically move to the line I care about with ]d, if you don't, you can change it to e.g. scope = 'buffer' to see it for all lines in the file.


Last updated: May 02 2025 at 03:31 UTC