Tweak infoview widgets style.

[gebner]

• [x] Less information by default (like pin number, undo list size, etc.)
• [ ] Hover tooltip shows type instead of "click here"
• [x] Map CR to click
• [x] Clean up hover tooltip (no "exprExplicit:", etc.)
• [x] Make highlight definitions work in GUI (only terminal colors provided atm)

[Julian]

I was doing the same thing locally :), you're faster at hitting the PR button. Will stop and let you deal with it given you've played with this longer, but yeah +1 on all the above.

[Julian]

I'm also probably in favor of mapping CR to click, which I think you mentioned somewhere else that I can't find, though I see it's not currently mapped.

[codecov[bot]]

Codecov Report

Merging #138 (23b7889) into main (73fedfd) will decrease coverage by 0.31%. The diff coverage is 28.12%.

:exclamation: Current head 23b7889 differs from pull request most recent head 20a8c83. Consider uploading reports for the commit 20a8c83 to get more accurate results

@@            Coverage Diff             @@
##             main     #138      +/-   ##
==========================================
- Coverage   81.99%   81.68%   -0.32%     
==========================================
  Files          39       39              
  Lines        3172     3172              
==========================================
- Hits         2601     2591      -10     
- Misses        571      581      +10     

Impacted Files	Coverage Δ
lua/lean/html.lua	53.33% <ø> (-0.94%)	:arrow_down:
lua/lean/infoview/components.lua	44.31% <13.33%> (+0.52%)	:arrow_up:
lua/lean/infoview.lua	81.75% <37.50%> (-1.98%)	:arrow_down:
lua/lean/rpc.lua	82.97% <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 26f95a4...20a8c83. Read the comment docs.

[Julian]

blehhh sorry I am dumb and accidentally merged this whilst trying it

[Julian]

(Fixing main, just letting you know)

[Julian]

(OK all clear, sorry for the noise.)

[gebner]

Okay, there's one thing left on the todo list but I'll merge the PR now.

What's missing is the "show tooltip when moving the cursor over a term" feature (right now you still need to click). From what I can tell this requires a bit of refactoring: 1) we should probably add events for entering/exiting a highlightable div. 2) these need to be hooked up so that they can cause a rerender (which I believe is handled with the call_event wrapper but I don't fully understand this part yet).

[Julian]

Sounds good to me, thanks!