Julian / lean.nvim

Neovim support for the Lean theorem prover
MIT License
277 stars 26 forks source link

Show stderr output in :messages #148

Closed gebner closed 3 years ago

gebner commented 3 years ago

Fixes #37.

codecov[bot] commented 3 years ago

Codecov Report

Merging #148 (f14acd4) into main (373c2e2) will increase coverage by 0.08%. The diff coverage is 100.00%.

Impacted file tree graph

@@            Coverage Diff             @@
##             main     #148      +/-   ##
==========================================
+ Coverage   81.39%   81.47%   +0.08%     
==========================================
  Files          39       40       +1     
  Lines        3192     3206      +14     
==========================================
+ Hits         2598     2612      +14     
  Misses        594      594              
Impacted Files Coverage Δ
lua/lean/init.lua 98.24% <100.00%> (+0.03%) :arrow_up:
lua/lean/stderr.lua 100.00% <100.00%> (ø)

Continue to review full report at Codecov.

Legend - Click here to learn more Δ = absolute <relative> (impact), ø = not affected, ? = missing data Powered by Codecov. Last update 373c2e2...f14acd4. Read the comment docs.

Julian commented 3 years ago

lgtm!

gebner commented 3 years ago

This might have been a bad idea because nvim_err_println steal the focus. If you get lots of stderr messages, then you can't edit the file anymore. Not even :q works...

Julian commented 3 years ago

Oy. Fair enough, back to print is all good with me.

gebner commented 3 years ago

I'm pretty sure that print has the same issue (afaict the only difference is that nvim_err_println prints in red).

Julian commented 3 years ago

Maybe we just make an infoview component then and shove lines into it?

gebner commented 3 years ago

Unfortunately the output becomes very long (and is obviously never reset), so I don't think this will fit into the infoview.

rish987 commented 3 years ago

Couldn't we put it into a tooltip or expandable component (like you did for traces)?

gebner commented 3 years ago

Mmh, we could put the last ten lines in the infoview and then open a new buffer (with the full stderr output) on enter.