[feat] Add Info View buttons: goto file/line/col#13
[feat] Add Info View buttons: goto file/line/col#13bollu wants to merge 3 commits intoleanprover-community:masterfrom
Conversation
This allows one to press <RET> on the link to go to the corresponding file/line/column.
bollu
left a comment
bollu
left a comment
There was a problem hiding this comment.
I've marked my concerns about the patch in the comments.
| (-lambda ((x &as &lean:PlainGoal? :goals)) | ||
| (setq lean4-goals goals) | ||
| (lean4-info-buffer-redisplay)) | ||
| (lean4-info-buffer-redisplay-debounced lsp-buffer-uri)) |
There was a problem hiding this comment.
I don't know if threading this state throughout the computation is idiomatic. Perhaps there is a nicer way to retrieve the URI that corresponds to a Goal/PlainGoal?
There was a problem hiding this comment.
Is this case different from the lean4-goals/term-goal defvars?
| (magit-insert-heading (format "%d:%d: " (1+ (lsp-translate-line line)) (lsp-translate-column character))) | ||
| (magit-insert-section (magit-section) | ||
| (magit-insert-heading) | ||
| (insert-button (format "%s %d:%d" uri (1+ (lsp-translate-line line)) (lsp-translate-column character)) |
There was a problem hiding this comment.
This prints out the raw URI, which is like:
file:///home/bollu/work/oss/lean4-metaprogramming-book/lean/extra/attributes.lean 56:0
I imagine there is a way to get the path relative to the LSP root, which I don't know yet.
There was a problem hiding this comment.
The info view will only ever show information from a single file anyway, no? So why include it at all?
| (magit-insert-heading (format "%d:%d: " (1+ (lsp-translate-line line)) (lsp-translate-column character))) | ||
| (magit-insert-section (magit-section) | ||
| (magit-insert-heading) | ||
| (insert-button (format "%s %d:%d" uri (1+ (lsp-translate-line line)) (lsp-translate-column character)) |
There was a problem hiding this comment.
I should style the button as if it were a magit header. It currently looks like a raw link. I haven't figured this out yet.
There was a problem hiding this comment.
I think the intended way is to modify the section's keymap, e.g. how RET in magit goes to whatever is underneath the cursor https://github.com/magit/magit/blob/4e29d5827cb77a7fbcff57033a099e23b8edd424/lisp/magit-status.el#L538-L540
| (magit-insert-heading) | ||
| (insert-button (format "%s %d:%d" uri (1+ (lsp-translate-line line)) (lsp-translate-column character)) | ||
| 'action (lambda (btn) | ||
| (with-current-buffer (find-file-other-window (lsp--uri-to-path uri)) |
There was a problem hiding this comment.
I imagine emacs has a nicer API to open the file and go to the correct file, line and column?
| (magit-insert-heading (format "%d:%d: " (1+ (lsp-translate-line line)) (lsp-translate-column character))) | ||
| (magit-insert-section (magit-section) | ||
| (magit-insert-heading) | ||
| (insert-button (format "%s %d:%d" uri (1+ (lsp-translate-line line)) (lsp-translate-column character)) |
There was a problem hiding this comment.
The info view will only ever show information from a single file anyway, no? So why include it at all?
| (magit-insert-heading (format "%d:%d: " (1+ (lsp-translate-line line)) (lsp-translate-column character))) | ||
| (magit-insert-section (magit-section) | ||
| (magit-insert-heading) | ||
| (insert-button (format "%s %d:%d" uri (1+ (lsp-translate-line line)) (lsp-translate-column character)) |
There was a problem hiding this comment.
I think the intended way is to modify the section's keymap, e.g. how RET in magit goes to whatever is underneath the cursor https://github.com/magit/magit/blob/4e29d5827cb77a7fbcff57033a099e23b8edd424/lisp/magit-status.el#L538-L540
| (-lambda ((x &as &lean:PlainGoal? :goals)) | ||
| (setq lean4-goals goals) | ||
| (lean4-info-buffer-redisplay)) | ||
| (lean4-info-buffer-redisplay-debounced lsp-buffer-uri)) |
There was a problem hiding this comment.
Is this case different from the lean4-goals/term-goal defvars?
4 participants
This allows one to press on the link to go to
the corresponding file/line/column.
Screenshot attached, where the section headers are now clickable links, that take one to the correct file/line/column