feat: lean4-mode: support plain goal view
This commit is contained in:
Sebastian Ullrich
parent
ec903f58d2
commit
f6359195aa
3 changed files with 28 additions and 175 deletions
|
|
@ -15,6 +15,7 @@
|
|||
;;
|
||||
|
||||
(require 'lean4-syntax)
|
||||
(require 'lsp-protocol)
|
||||
|
||||
;; Lean Info Mode (for "*lean4-info*" buffer)
|
||||
;; Automode List
|
||||
|
|
@ -58,57 +59,30 @@
|
|||
;; current window of current buffer is selected (i.e., in focus)
|
||||
(eq (current-buffer) (window-buffer))))
|
||||
|
||||
(defun lean4-get-info-record-at-point (cont)
|
||||
"Get info-record at the current point"
|
||||
(with-demoted-errors "lean get info: %s"
|
||||
(lean4-server-send-command
|
||||
'info (list :file_name (buffer-file-name)
|
||||
:line (line-number-at-pos)
|
||||
:column (lean4-line-offset))
|
||||
(cl-function
|
||||
(lambda (&key record)
|
||||
(funcall cont record))))))
|
||||
(lsp-interface
|
||||
(lean:PlainGoal (:rendered) nil))
|
||||
|
||||
(defun lean4-info-right-click-find-definition ()
|
||||
"Offer to jump to definition of right-click target."
|
||||
(defconst lean4-show-goal-buffer-name "*Lean Goal*")
|
||||
|
||||
(defun lean4-show-goal--handler ()
|
||||
(let ((deactivate-mark)) ; keep transient mark
|
||||
(when (lean4-info-buffer-active lean4-show-goal-buffer-name)
|
||||
(lsp-request-async
|
||||
"$/lean/plainGoal"
|
||||
(lsp--text-document-position-params)
|
||||
(-lambda ((goal &as &lean:PlainGoal? :rendered))
|
||||
(when goal
|
||||
(let ((rerendered (lsp--render-string rendered "markdown")))
|
||||
(lean4-with-info-output-to-buffer lean4-show-goal-buffer-name
|
||||
(insert rerendered)))))
|
||||
:error-handler #'ignore
|
||||
:mode 'tick
|
||||
:cancel-token :plain-goal))))
|
||||
|
||||
(defun lean4-toggle-show-goal ()
|
||||
"Show goal at the current point."
|
||||
(interactive)
|
||||
(list 'info
|
||||
(list :file_name (buffer-file-name)
|
||||
:line (line-number-at-pos)
|
||||
:column (lean4-line-offset))
|
||||
(cl-function
|
||||
(lambda (&key record)
|
||||
(let ((source-record (plist-get record :source)))
|
||||
(if source-record
|
||||
(let ((full-name (plist-get record :full-id)))
|
||||
(list
|
||||
(list :name (if full-name
|
||||
(concat "Find definition of " full-name)
|
||||
"Find definition")
|
||||
:action (lambda ()
|
||||
(apply #'lean4-find-definition-cont source-record)))))
|
||||
(list)))))))
|
||||
|
||||
(cl-defun lean4-find-definition-cont (&key file line column)
|
||||
(when (fboundp 'xref-push-marker-stack) (xref-push-marker-stack))
|
||||
(when file
|
||||
(find-file file))
|
||||
(goto-char (point-min))
|
||||
(forward-line (1- line))
|
||||
(forward-char column))
|
||||
|
||||
|
||||
(defun lean4-find-definition ()
|
||||
"Jump to definition of thing at point"
|
||||
(interactive)
|
||||
(setq lean4-show-goal--handler-mask t) ; avoid the current request to the Lean server to by
|
||||
; interrupted by requests made for `lean4-show-goal`
|
||||
(lean4-get-info-record-at-point
|
||||
(lambda (info-record)
|
||||
(-if-let (source-record (plist-get info-record :source))
|
||||
(apply #'lean4-find-definition-cont source-record)
|
||||
(-if-let (id (plist-get info-record :full-id))
|
||||
(message "no source location available for %s" id)
|
||||
(message "unknown thing at point"))))))
|
||||
(lean4-toggle-info-buffer lean4-show-goal-buffer-name)
|
||||
(lean4-show-goal--handler))
|
||||
|
||||
(provide 'lean4-info)
|
||||
|
|
|
|||
|
|
@ -31,6 +31,7 @@
|
|||
(require 'dash)
|
||||
(require 'pcase)
|
||||
(require 'flycheck)
|
||||
(require 'lsp-mode)
|
||||
(require 'lean4-eri)
|
||||
(require 'lean4-util)
|
||||
(require 'lean4-settings)
|
||||
|
|
@ -39,9 +40,8 @@
|
|||
(require 'lean4-leanpkg)
|
||||
;(require 'lean4-server)
|
||||
(require 'lean4-flycheck)
|
||||
;(require 'lean4-info)
|
||||
(require 'lean4-info)
|
||||
;(require 'lean4-hole)
|
||||
;(require 'lean4-type)
|
||||
;(require 'lean4-message-boxes)
|
||||
;(require 'lean4-right-click)
|
||||
(require 'lean4-dev)
|
||||
|
|
@ -89,16 +89,6 @@
|
|||
:version lsp--cur-version
|
||||
:text (lsp--buffer-content)))))
|
||||
|
||||
(defun lean4-check-expansion ()
|
||||
(interactive)
|
||||
(save-excursion
|
||||
(if (looking-at (rx symbol-start "_")) t
|
||||
(if (looking-at "\\_>") t
|
||||
(backward-char 1)
|
||||
(if (looking-at "\\.") t
|
||||
(backward-char 1)
|
||||
(if (looking-at "->") t nil))))))
|
||||
|
||||
(defun lean4-tab-indent ()
|
||||
(interactive)
|
||||
(cond ((looking-back (rx line-start (* white)) nil)
|
||||
|
|
@ -169,7 +159,7 @@
|
|||
;; Handle events that may start automatic syntax checks
|
||||
(before-save-hook . lean4-whitespace-cleanup)
|
||||
;; info windows
|
||||
;; (post-command-hook . lean4-show-goal--handler)
|
||||
(post-command-hook . lean4-show-goal--handler)
|
||||
(post-command-hook . lean4-next-error--handler)
|
||||
;; (flycheck-after-syntax-check-hook . lean4-show-goal--handler)
|
||||
(flycheck-after-syntax-check-hook . lean4-next-error--handler)
|
||||
|
|
@ -231,10 +221,9 @@ Invokes `lean4-mode-hook'.
|
|||
(modify-coding-system-alist 'file "\\.lean\\'" 'utf-8)
|
||||
|
||||
;; LSP init
|
||||
(require 'lsp-mode)
|
||||
;; Ref: https://emacs-lsp.github.io/lsp-mode/page/adding-new-language/
|
||||
(add-to-list 'lsp-language-id-configuration
|
||||
'(lean4-mode . "lean4"))
|
||||
'(lean4-mode . "lean"))
|
||||
|
||||
(lsp-register-client
|
||||
(make-lsp-client :new-connection (lsp-stdio-connection (lambda () `(,(lean4-get-executable lean4-executable-name) "--server")))
|
||||
|
|
|
|||
|
|
@ -1,110 +0,0 @@
|
|||
;; -*- lexical-binding: t; -*-
|
||||
;; Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
;; Released under Apache 2.0 license as described in the file LICENSE.
|
||||
;;
|
||||
;; Authors: Soonho Kong, Sebastian Ullrich
|
||||
;;
|
||||
|
||||
(require 'cl-lib)
|
||||
(require 'dash)
|
||||
(require 'dash-functional)
|
||||
(require 's)
|
||||
(require 'lean4-util)
|
||||
;(require 'lean4-server)
|
||||
(require 'lean4-debug)
|
||||
(require 'flymake)
|
||||
|
||||
(defun lean4-fill-placeholder-cont (info-record)
|
||||
"Continuation for lean4-fill-placeholder"
|
||||
(let ((synth (and info-record (plist-get info-record :synth))))
|
||||
(when synth
|
||||
(let ((synth-str
|
||||
(replace-regexp-in-string "?M_[0-9]+" "_" synth)))
|
||||
(when (cl-search " " synth-str)
|
||||
(setq synth-str (concat "(" synth-str ")")))
|
||||
(when (looking-at "_")
|
||||
(delete-char 1)
|
||||
(insert synth-str))))))
|
||||
|
||||
(defun lean4-fill-placeholder ()
|
||||
"Fill the placeholder with a synthesized expression by Lean."
|
||||
(interactive)
|
||||
(lean4-get-info-record-at-point 'lean4-fill-placeholder-cont))
|
||||
|
||||
(cl-defun lean4-info-record-to-string (info-record)
|
||||
"Given typeinfo, overload, and sym-name, compose information as a string."
|
||||
(destructuring-bind (&key type tactic_params tactic_param_idx text doc full-id &allow-other-keys) info-record
|
||||
(let ((name-str (or full-id text))
|
||||
(type-str type)
|
||||
str)
|
||||
(when tactic_params
|
||||
(setq tactic_params (-map-indexed (lambda (i param)
|
||||
(if (eq i tactic_param_idx)
|
||||
(propertize param 'face 'eldoc-highlight-function-argument)
|
||||
param)) tactic_params))
|
||||
(setq type-str (mapconcat 'identity tactic_params " ")))
|
||||
|
||||
(when (and name-str type-str)
|
||||
(setq str (format (if tactic_params "%s %s" "%s : %s")
|
||||
(propertize name-str 'face 'font-lock-variable-name-face)
|
||||
type-str)))
|
||||
(when doc
|
||||
(let* ((lines (split-string doc "\n"))
|
||||
(doc (if (cdr lines)
|
||||
(concat (car lines) " ⋯")
|
||||
(car lines))))
|
||||
(setq str (concat str
|
||||
(format "\n%s"
|
||||
(propertize doc 'face 'font-lock-comment-face))))))
|
||||
str)))
|
||||
|
||||
(defvar-local lean4-eldoc-documentation-cache nil)
|
||||
|
||||
(defun lean4-eldoc-documentation-function-cont (info-record &optional add-to-kill-ring)
|
||||
"Continuation for lean4-eldoc-documentation-function"
|
||||
(let ((info-string (and info-record (lean4-info-record-to-string info-record))))
|
||||
(when info-string
|
||||
(when add-to-kill-ring
|
||||
(kill-new
|
||||
(substring-no-properties info-string))))
|
||||
(setq lean4-eldoc-documentation-cache (and info-string (format "%s" info-string)))
|
||||
(eldoc-message lean4-eldoc-documentation-cache)))
|
||||
|
||||
(defun lean4-eldoc-documentation-function (&optional add-to-kill-ring)
|
||||
"Show information of lean expression at point if any"
|
||||
(interactive)
|
||||
(when (not (eq lean4-server-check-mode 'nothing)) ; TODO(gabriel): revisit once info no longer reparses the file
|
||||
(lean4-get-info-record-at-point
|
||||
(lambda (info-record)
|
||||
(lean4-eldoc-documentation-function-cont info-record add-to-kill-ring)))
|
||||
lean4-eldoc-documentation-cache))
|
||||
|
||||
(defun lean4-show-type ()
|
||||
"Show information of lean4-expression at point if any."
|
||||
(interactive)
|
||||
(lean4-eldoc-documentation-function lean4-show-type-add-to-kill-ring))
|
||||
|
||||
(defconst lean4-show-goal-buffer-name "*Lean Goal*")
|
||||
|
||||
(setq lean4-show-goal--handler-mask nil)
|
||||
|
||||
(defun lean4-show-goal--handler ()
|
||||
(if lean4-show-goal--handler-mask
|
||||
(setq lean4-show-goal--handler-mask nil)
|
||||
(let ((deactivate-mark)) ; keep transient mark
|
||||
(when (and (not (eq lean4-server-check-mode 'nothing))
|
||||
; TODO(gabriel): revisit ^^ once info no longer reparses the file
|
||||
(lean4-info-buffer-active lean4-show-goal-buffer-name))
|
||||
(lean4-get-info-record-at-point
|
||||
(lambda (info-record)
|
||||
(let ((state (plist-get info-record :state)))
|
||||
(unless (or (s-blank? state) (s-blank? (s-trim state)))
|
||||
(lean4-with-info-output-to-buffer lean4-show-goal-buffer-name (princ state))))))))))
|
||||
|
||||
(defun lean4-toggle-show-goal ()
|
||||
"Show goal at the current point."
|
||||
(interactive)
|
||||
(lean4-toggle-info-buffer lean4-show-goal-buffer-name)
|
||||
(lean4-show-goal--handler))
|
||||
|
||||
(provide 'lean4-type)
|
||||
Loading…
Add table
Reference in a new issue