max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(emacs): remove unused options

Browse source
This commit is contained in:
Gabriel Ebner 2017-01-18 08:53:02 +01:00 • committed by Leonardo de Moura
parent b309ef66d7
commit 9530a7db1c
3 changed files with 0 additions and 43 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/emacs/lean-flycheck.el
View file

@ -77,9 +77,6 @@
;; If "*Flycheck errors" buffer is available, use its width
(flycheck-error-window
(window-body-width flycheck-error-window))
;; If lean-flycheck-msg-width is set, use it
(lean-flycheck-msg-width
lean-flycheck-msg-width)
;; Can we split vertically?
((window-splittable-p window nil)
body-width)

4
src/emacs/lean-mode.el
View file

@ -93,9 +93,6 @@
(local-set-key lean-keybinding-lean-toggle-next-error 'lean-toggle-next-error)
)
(defun lean-define-key-binding (key cmd)
(local-set-key key `(lambda () (interactive) ,cmd)))
(define-abbrev-table 'lean-abbrev-table
'())
@ -113,7 +110,6 @@
["Toggle next error display" lean-toggle-next-error t]
["Find definition at point" lean-find-definition t]
"-----------------"
["Run flycheck" flycheck-compile (and lean-flycheck-use flycheck-mode)]
["List of errors" flycheck-list-errors (and lean-flycheck-use flycheck-mode)]
"-----------------"
["Restart lean process" lean-server-restart t]

36
src/emacs/lean-settings.el
View file

@ -64,23 +64,6 @@
:group 'lean
:type 'boolean)
(defcustom lean-flycheck-max-messages-to-display 100
"Maximum number of flycheck messages to displaylean-flychecker checker name
(Restart required to be effective)"
:group 'lean
:type 'number)
(defcustom lean-default-pp-width 120
"Width of Lean error/warning messages"
:group 'lean
:type 'number)
(defcustom lean-flycheck-msg-width nil
"Width of Lean error/warning messages"
:group 'lean
:type '(choice (const :tag "Let lean-mode automatically detect this" nil)
(integer :tag "Specify the value and force lean-mode to use")))
(defcustom lean-delete-trailing-whitespace nil
"Set this variable to true to automatically delete trailing
whitespace when a buffer is loaded from a file or when it is
@ -88,12 +71,6 @@ written."
:group 'lean
:type 'boolean)
(defcustom lean-debug-mode-line '(:eval (lean-debug-mode-line-status-text))
"Mode line lighter for Lean debug mode."
:group 'lean
:type 'sexp
:risky t)
(defcustom lean-show-type-add-to-kill-ring nil
"If it is non-nil, add the type information to the kill-ring so
that user can yank(paste) it later. By default, it's
@ -101,13 +78,6 @@ false (nil)."
:group 'lean
:type 'boolean)
(defcustom lean-proofstate-display-style 'show-first-and-other-conclusions
"Choose how to display proof state in *lean-info* buffer."
:group 'lean
:type '(choice (const :tag "Show all goals" show-all)
(const :tag "Show only the first" show-first)
(const :tag "Show the first goal, and the conclusions of all other goals" show-first-and-other-conclusions)))
(defcustom lean-keybinding-std-exe1 (kbd "C-c C-x")
"Lean Keybinding for std-exe #1"
:group 'lean-keybinding :type 'key-sequence)
@ -117,12 +87,6 @@ false (nil)."
(defcustom lean-keybinding-show-key (kbd "C-c C-k")
"Lean Keybinding for show-key"
:group 'lean-keybinding :type 'key-sequence)
(defcustom lean-keybinding-set-option (kbd "C-c C-o")
"Lean Keybinding for set-option"
:group 'lean-keybinding :type 'key-sequence)
(defcustom lean-keybinding-eval-cmd (kbd "C-c C-e")
"Lean Keybinding for eval-cmd"
:group 'lean-keybinding :type 'key-sequence)
(defcustom lean-keybinding-server-restart (kbd "C-c C-r")
"Lean Keybinding for server-restart"
:group 'lean-keybinding :type 'key-sequence)