Julian / lean.nvim

neovim support for the Lean theorem prover
MIT License
255 stars 25 forks source link

Add an option to open the infoview in an entirely new tab. #269

Closed tage64 closed 2 years ago

tage64 commented 2 years ago

This pull request adds an option (infoview.separate_tab: bool) which if set to true will cause the infoview to be opened in a new tabpage rather then in a horizontal or vertical split of the current window.

This is probably not useful for most users since one will not be able to see real time changes in the infoview. But I'm using a screen reader which speaks all dynamic changes in the terminal immediately. And it sometimes become too much information at the same time when it speaks both changes in the main buffer and the infoview.

A better solution would of course be to make the screen reader smarter so that it can recognize horizontally/verticly split windows and only speak changes in the current window. But that was too complicated for a Sunday evening so I decided to change this pluggin instead.

I'm not an expert in Lua, so feel free to comment or improve my changes.

I would understand if you think the audience for this feature is very limited. It might be that there will only be me and other visually impared people who make use of this feature. But the changes are very small though, so I hope you have no problems to merge it.