From f6359195aa6ff1420d21c61395a1bdf93e54aabd Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sat, 6 Feb 2021 17:23:52 +0100 Subject: [PATCH] feat: lean4-mode: support plain goal view --- lean4-mode/lean4-info.el | 74 +++++++++----------------- lean4-mode/lean4-mode.el | 19 ++----- lean4-mode/lean4-type.el | 110 --------------------------------------- 3 files changed, 28 insertions(+), 175 deletions(-) delete mode 100644 lean4-mode/lean4-type.el diff --git a/lean4-mode/lean4-info.el b/lean4-mode/lean4-info.el index 9b0d463813..5e665a1e81 100644 --- a/lean4-mode/lean4-info.el +++ b/lean4-mode/lean4-info.el @@ -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) diff --git a/lean4-mode/lean4-mode.el b/lean4-mode/lean4-mode.el index 60473ae508..5c74c2428f 100644 --- a/lean4-mode/lean4-mode.el +++ b/lean4-mode/lean4-mode.el @@ -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"))) diff --git a/lean4-mode/lean4-type.el b/lean4-mode/lean4-type.el deleted file mode 100644 index 6c57a23223..0000000000 --- a/lean4-mode/lean4-type.el +++ /dev/null @@ -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)