diff --git a/src/emacs/lean-flycheck.el b/src/emacs/lean-flycheck.el deleted file mode 100644 index e0b6488051..0000000000 --- a/src/emacs/lean-flycheck.el +++ /dev/null @@ -1,143 +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. -;; -;; Author: Soonho Kong -;; -(require 'flycheck) -(require 'lean-settings) -(require 'lean-server) -(require 'lean-info) - -(defun lean-toggle-flycheck-mode () - "Toggle flycheck-mode" - (interactive) - (cond - (flycheck-mode (flycheck-mode -1)) - (t (flycheck-mode 1)))) - -(cl-defun lean-flycheck-parse-task (checker buffer cur-file-name - &key pos_line pos_col desc file_name &allow-other-keys) - (if (equal cur-file-name file_name) - (flycheck-error-new-at pos_line (1+ pos_col) - 'info - (format "still running: %s" desc) - :filename file_name - :checker checker :buffer buffer) - (flycheck-error-new-at 1 1 - 'info - (format "still running: %s" desc) - :filename cur-file-name - :checker checker :buffer buffer))) - -(defun lean-flycheck-mk-task-msgs (checker buffer sess) - (if (and sess (lean-server-session-tasks sess) - (plist-get (lean-server-session-tasks sess) :is_running)) - (let* ((cur-fn (buffer-file-name)) - (tasks (lean-server-session-tasks sess)) - (cur-task (plist-get tasks :cur_task)) - (tasks-for-cur-file (remove-if-not (lambda (task) (equal cur-fn (plist-get task :file_name))) - (plist-get tasks :tasks))) - (display-tasks)) - ;; do not display tasks for current file when highlighting is enabled - (when (not lean-server-show-pending-tasks) - (setq display-tasks tasks-for-cur-file)) - ;; show current task when not in current file - (when (and cur-task - (not (equal cur-fn (plist-get cur-task :file_name)))) - (setq display-tasks (cons cur-task display-tasks))) - (mapcar (lambda (task) (apply #'lean-flycheck-parse-task checker buffer cur-fn task)) - display-tasks)))) - -(cl-defun lean-flycheck-parse-error (checker buffer &key pos_line pos_col severity text file_name &allow-other-keys) - (flycheck-error-new-at pos_line (1+ pos_col) - (pcase severity - ("error" 'error) - ("warning" 'warning) - ("information" 'info) - (_ 'info)) - (lean-highlight-string text) - :filename file_name - :checker checker :buffer buffer)) - -(defun lean-flycheck-start (checker callback) - (let ((cur-fn (buffer-file-name)) - (buffer (current-buffer))) - (funcall callback 'finished - (if lean-server-session - (append - (lean-flycheck-mk-task-msgs checker buffer lean-server-session) - (mapcar (lambda (msg) (apply #'lean-flycheck-parse-error checker buffer msg)) - (remove-if-not (lambda (msg) (equal cur-fn (plist-get msg :file_name))) - (lean-server-session-messages lean-server-session)))))))) - -(defun lean-flycheck-init () - "Initialize lean-flychek checker" - (flycheck-define-generic-checker 'lean-checker - "A Lean syntax checker." - :start #'lean-flycheck-start - :modes '(lean-mode)) - (add-to-list 'flycheck-checkers 'lean-checker)) - -(defun lean-flycheck-turn-on () - (flycheck-mode t)) - -(defun lean-flycheck-error-list-buffer-width () - "Return the width of flycheck-error list buffer" - (interactive) - (let* ((flycheck-error-window (get-buffer-window "*Flycheck errors*" t)) - (window (selected-window)) - (body-width (window-body-width window))) - (cond - ;; If "*Flycheck errors" buffer is available, use its width - (flycheck-error-window - (window-body-width flycheck-error-window)) - ;; Can we split vertically? - ((window-splittable-p window nil) - body-width) - ;; Can we split horizontally? - ((window-splittable-p window t) - (/ body-width 2)) - ;; In worst case, just use the same width of current window - (t body-width)))) - -(defun lean-flycheck-error-list-message-width () - "Return the width of error messages in the flycheck-error list buffer" - (let (;; assume 'Message' is last column and has size 0 (true for default config) - (other-columns-width (apply '+ (mapcar (apply-partially 'nth 1) flycheck-error-list-format))) - (margin (length flycheck-error-list-format))) - (cond - ;; If lean-flycheck-msg-width is set, use it - (lean-flycheck-msg-width - lean-flycheck-msg-width) - (t (- (lean-flycheck-error-list-buffer-width) other-columns-width margin))))) - -(defconst lean-next-error-buffer-name "*Lean Next Error*") - -(defun lean-next-error--handler () - (when (lean-info-buffer-active lean-next-error-buffer-name) - (let ((deactivate-mark) ; keep transient mark - (errors (or - ;; prefer error of current position, if any - (flycheck-overlay-errors-at (point)) - ;; try errors in current line next - (sort (flycheck-overlay-errors-in (line-beginning-position) (line-end-position)) - #'flycheck-error-<) - ;; fall back to next error position - (-if-let* ((pos (flycheck-next-error-pos 1))) - (flycheck-overlay-errors-at pos))))) - (lean-with-info-output-to-buffer lean-next-error-buffer-name - (dolist (e errors) - (princ (format "%d:%d: " (flycheck-error-line e) (flycheck-error-column e))) - (princ (flycheck-error-message e)) - (princ "\n\n")) - (when flycheck-current-errors - (princ (format "(%d more messages above...)" (length flycheck-current-errors)))))))) - -(defun lean-toggle-next-error () - (interactive) - (lean-toggle-info-buffer lean-next-error-buffer-name) - (lean-next-error--handler)) - -(provide 'lean-flycheck) diff --git a/src/emacs/lean-type.el b/src/emacs/lean-type.el deleted file mode 100644 index ad77700d04..0000000000 --- a/src/emacs/lean-type.el +++ /dev/null @@ -1,174 +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 'lean-util) -(require 'lean-server) -(require 'lean-debug) -(require 'flymake) - -(defun lean-toggle-eldoc-mode () - "Toggle eldoc-mode" - (interactive) - (cond - (eldoc-mode (eldoc-mode -1)) - (t (eldoc-mode 1)))) - -(defun lean-fill-placeholder-cont (info-record) - "Continuation for lean-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-forward-char 1) - (insert synth-str)))))) - -(defun lean-fill-placeholder () - "Fill the placeholder with a synthesized expression by Lean." - (interactive) - (lean-get-info-record-at-point 'lean-fill-placeholder-cont)) - -(cl-defun lean-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 overloads synth coercion proofstate full-id symbol extra &allow-other-keys) info-record - (let (name-str type-str coercion-str extra-str proofstate-str overload-str stale-str str) - (setq name-str - (cond - (synth synth) - ((and full-id symbol) - (format "[%s] %s" symbol full-id)) - (t (or full-id text symbol)))) - (when coercion - (destructuring-bind (&key expr type) coercion - (setq coercion-str - (format "%s : %s" - (propertize expr 'face 'font-lock-variable-name-face) - type)))) - (when type - (setq type-str (lean-highlight-string type))) - (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 overloads - (setq overload-str (s-join ", " overloads))) - (when extra - (destructuring-bind (&key expr type) extra - (setq str - (cond (lean-show-only-type-in-parens (format ": %s" type)) - (t (format "(%s) : %s" - (propertize expr 'face 'font-lock-variable-name-face) - type)))))) - (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 (and str coercion-str) - (setq str (format "%s\n%s %s" - str - (propertize "coercion applied" 'face 'font-lock-keyword-face) - coercion-str))) - (when overload-str - (setq str (concat str - (format "\n%s with %s" - (propertize "overloaded" 'face 'font-lock-keyword-face) - overload-str)))) - (when proofstate - (setq str proofstate)) - (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 lean-eldoc-documentation-cache nil) - -(defun lean-eldoc-documentation-function-cont (info-record &optional add-to-kill-ring) - "Continuation for lean-eldoc-documentation-function" - (let ((info-string (and info-record (lean-info-record-to-string info-record)))) - (when info-string - (when add-to-kill-ring - (kill-new - (substring-no-properties info-string)))) - (setq lean-eldoc-documentation-cache (and info-string (format "%s" info-string))) - (eldoc-message lean-eldoc-documentation-cache))) - -(defun lean-eldoc-documentation-function (&optional add-to-kill-ring) - "Show information of lean expression at point if any" - (interactive) - (when (not (eq lean-server-check-mode 'nothing)) ; TODO(gabriel): revisit once info no longer reparses the file - (lean-get-info-record-at-point - (lambda (info-record) - (lean-eldoc-documentation-function-cont info-record add-to-kill-ring))) - lean-eldoc-documentation-cache)) - -(defun lean-show-type () - "Show information of lean-expression at point if any." - (interactive) - (lean-eldoc-documentation-function lean-show-type-add-to-kill-ring)) - -(defconst lean-show-goal-buffer-name "*Lean Goal*") - -(defun lean-show-goal--handler () - (let ((deactivate-mark)) ; keep transient mark - (when (and (not (eq lean-server-check-mode 'nothing)) - ; TODO(gabriel): revisit ^^ once info no longer reparses the file - (lean-info-buffer-active lean-show-goal-buffer-name)) - (lean-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))) - (lean-with-info-output-to-buffer lean-show-goal-buffer-name (princ state))))))))) - -(defun lean-toggle-show-goal () - "Show goal at the current point." - (interactive) - (lean-toggle-info-buffer lean-show-goal-buffer-name) - (lean-show-goal--handler)) - -(defun lean-helm-definitions-format-candidate (c) - `(,(format "%s : %s %s" - (propertize (plist-get c :text) 'face font-lock-variable-name-face) - (plist-get c :type) - (propertize (plist-get (plist-get c :source) :file) 'face font-lock-comment-face)) - . ,c)) - -(defun lean-helm-definitions-candidates () - (with-helm-current-buffer - (let* ((response (lean-server-send-synchronous-command 'search (list :query helm-pattern))) - (results (plist-get response :results)) - (results (-filter (lambda (c) (plist-get c :source)) results)) - (candidates (-map 'lean-helm-definitions-format-candidate results))) - candidates))) - -(defun lean-helm-definitions () - "Open a 'helm' interface for searching Lean definitions." - (interactive) - (require 'helm) - (helm :sources (helm-build-sync-source "helm-source-lean-definitions" - :requires-pattern t - :candidates 'lean-helm-definitions-candidates - :volatile t - :match 'identity - :action '(("Go to" . (lambda (c) (with-helm-current-buffer - (apply 'lean-find-definition-cont (plist-get c :source))))))) - :buffer "*helm Lean definitions*")) - -(provide 'lean-type)