Julian / lean.nvim

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

Make stderr window height configurable and fix autoscroll. #280

Closed rish987 closed 1 year ago

rish987 commented 1 year ago

I've been dealing with very long repr traces recently so this would be very nice to have, just wanted to make sure we agree on the option name/location.

Edit: Also added an "autoscroll" to automatically go to the end of the trace when we get new output. Wait we already have this? But it wasn't working for me, hmm Fixed.

Julian commented 1 year ago

Feature seems reasonable to me, though yeah think maybe it'd be a bit more consistent to use the option name we use for the infoview (i.e. width and/or height and/or horizontal_position if we even support splitting stderr vertically, I forget).

rish987 commented 1 year ago

Good point, just renamed it to "height" (as it seems we don't support a vertical split atm). Also squeezed in a fix for the autoscroll functionality.

Julian commented 1 year ago

Cool, haven't tested it out but lgtm if/when it works and passes CI