Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[feat] Add Info View buttons: goto file/line/col #13

Draft
wants to merge 3 commits into
base: master
Choose a base branch
from
Draft

[feat] Add Info View buttons: goto file/line/col #13

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
df59b9e
[feat] Add Info View buttons: goto file/line/col
bollu Jun 2, 2022
439346e
Cleanup dead code
bollu Jun 2, 2022
25fbc19
Cleanup debug messaging
bollu Jun 2, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
28 changes: 17 additions & 11 deletions lean4-info.el
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -82,19 +82,25 @@
(lsp-defun lean4-diagnostic-full-end-line ((&lean:Diagnostic :full-range (&Range :end (&Position :line))))
line)

(defun lean4-mk-message-section (caption errors)
(defun lean4-mk-message-section (uri caption errors)
(when errors
(magit-insert-section (magit-section)
(magit-insert-heading caption)
(magit-insert-section-body
(dolist (e errors)
(-let (((&Diagnostic :message :range (&Range :start (&Position :line :character))) e))
(magit-insert-section (magit-section)
(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))
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The info view will only ever show information from a single file anyway, no? So why include it at all?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

'action (lambda (btn)
(with-current-buffer (find-file-other-window (lsp--uri-to-path uri))
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I imagine emacs has a nicer API to open the file and go to the correct file, line and column?

(goto-line (lsp-translate-line line))
(move-to-column (lsp-translate-column character)))))
(insert "\n")
(magit-insert-section-body
(insert message "\n")))))))))

(defun lean4-info-buffer-redisplay ()
(defun lean4-info-buffer-redisplay (uri)
(when (lean4-info-buffer-active lean4-info-buffer-name)
(-let* ((deactivate-mark) ; keep transient mark
(pos (apply #'lsp-make-position (lsp--cur-position)))
Expand All @@ -121,9 +127,9 @@
(magit-insert-heading "Expected type:")
(magit-insert-section-body
(insert (lsp--fontlock-with-mode lean4-term-goal 'lean4-info-mode) "\n"))))
(lean4-mk-message-section "Messages here:" errors-here)
(lean4-mk-message-section "Messages below:" errors-below)
(lean4-mk-message-section "Messages above:" errors-above)
(lean4-mk-message-section uri "Messages here:" errors-here)
(lean4-mk-message-section uri "Messages below:" errors-below)
(lean4-mk-message-section uri "Messages above:" errors-above)
(when lean4-highlight-inaccessible-names
(goto-char 0)
(while (re-search-forward "\\(\\sw+\\)✝\\([¹²³⁴-⁹⁰]*\\)" nil t)
Expand All @@ -137,18 +143,18 @@
(lsp-request-async
"$/lean/plainGoal"
(lsp--text-document-position-params)
(-lambda ((_ &as &lean:PlainGoal? :goals))
(-lambda ((x &as &lean:PlainGoal? :goals))
(setq lean4-goals goals)
(lean4-info-buffer-redisplay))
(lean4-info-buffer-redisplay-debounced lsp-buffer-uri))
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this case different from the lean4-goals/term-goal defvars?

:error-handler #'ignore
:mode 'tick
:cancel-token :plain-goal)
(lsp-request-async
"$/lean/plainTermGoal"
(lsp--text-document-position-params)
(-lambda ((_ &as &lean:PlainTermGoal? :goal))
(-lambda ((x &as &lean:PlainTermGoal? :goal))
(setq lean4-term-goal goal)
(lean4-info-buffer-redisplay))
(lean4-info-buffer-redisplay-debounced lsp-buffer-uri))
:error-handler #'ignore
:mode 'tick
:cancel-token :plain-term-goal)
Expand Down