chore(emacs): remove obsolete files
This commit is contained in:
Sebastian Ullrich
parent
0388dd9640
commit
55276a5c36
2 changed files with 0 additions and 317 deletions
|
|
@ -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)
|
||||
|
|
@ -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)
|
||||
Loading…
Add table
Reference in a new issue