diff --git a/src/emacs/lean-company.el b/src/emacs/lean-company.el index 09e4fc89f..dae121df1 100644 --- a/src/emacs/lean-company.el +++ b/src/emacs/lean-company.el @@ -10,6 +10,7 @@ (require 'dash-functional) (require 'f) (require 's) +(require 'cl-lib) (require 'lean-util) (require 'lean-tags) (require 'lean-server) @@ -106,7 +107,7 @@ `(,file-name . 1))) (defun company-lean--import (command &optional arg &rest ignored) - (case command + (cl-case command (prefix (company-lean--import-prefix)) (candidates (company-lean--import-candidates arg)) (location (company-lean--import-location arg)) @@ -146,7 +147,7 @@ (--filter (s-starts-with? prefix it) candidates))) (defun company-lean--option-name (command &optional arg &rest ignored) - (case command + (cl-case command (prefix (company-lean--option-name-prefix)) (candidates (company-lean--option-name-candidates arg)) (meta (company-lean--option-name-meta arg)) @@ -180,7 +181,7 @@ (delete-forward-char 1))) (defun company-lean--findg (command &optional arg &rest ignored) - (case command + (cl-case command (prefix (company-lean--findg-prefix)) (candidates (company-lean--findg-candidates arg)) (annotation (company-lean--findp-annotation arg)) @@ -290,7 +291,7 @@ triggers a completion immediately." 0))) (defun company-lean--findp (command &optional arg &rest ignored) - (case command + (cl-case command (prefix (company-lean--findp-prefix)) (candidates (company-lean--findp-candidates arg)) (annotation (company-lean--findp-annotation arg)) diff --git a/src/emacs/lean-info.el b/src/emacs/lean-info.el index d4676b158..a041997c1 100644 --- a/src/emacs/lean-info.el +++ b/src/emacs/lean-info.el @@ -198,7 +198,7 @@ (string-join (lean-info-symbol-body symbol) "\n")) (defun lean-info-id-symbol-body-str (info) - (case (lean-info-kind info) + (cl-case (lean-info-kind info) ('IDENTIFIER (string-join (lean-info-symbol-body info) "\n")) ('SYMBOL (string-join (lean-info-identifier-body info) "\n")))) diff --git a/src/emacs/lean-type.el b/src/emacs/lean-type.el index c802be685..e400c0c80 100644 --- a/src/emacs/lean-type.el +++ b/src/emacs/lean-type.el @@ -29,7 +29,7 @@ (when synth (let ((synth-str (replace-regexp-in-string "?M_[0-9]+" "_" (lean-info-synth-body-str synth)))) - (when (search " " synth-str) + (when (cl-search " " synth-str) (setq synth-str (concat "(" synth-str ")"))) (when (looking-at "_") (delete-forward-char 1)