fix(emacs): void-function in lean-debug-mode

This commit is contained in:
Sebastian Ullrich 2016-10-14 13:52:08 -04:00 committed by Leonardo de Moura
parent 7e570d7777
commit 8f71f4c82d
2 changed files with 3 additions and 12 deletions

View file

@ -48,16 +48,7 @@
(defun lean-debug-mode-line-status-text ()
"Get a text describing STATUS for use in the mode line."
(let ((text
;; No Process : "X"
(cond ((not (lean-server-process-exist-p))
"X")
;; Number of Async Queue: *-n
((> (lean-server-async-task-queue-len) 0)
(format "*-%d" (lean-server-async-task-queue-len)))
;; Async Queue = 0
(t ""))))
(concat " LeanDebug" text)))
"LeanDebug")
(define-minor-mode lean-debug-mode
"Minor mode for lean debugging."

View file

@ -277,8 +277,8 @@ json server::handle_complete(json const & req) {
std::vector<pair<std::string, name>> selected;
bitap_fuzzy_search matcher(pattern, max_errors);
env.for_each_declaration([&](declaration const & d) {
/*if (is_projection(env, d.get_name()))
return;*/
if (is_projection(env, d.get_name()))
return;
if (auto it = exact_prefix_match(env, pattern, d)) {
exact_matches.emplace_back(*it, d.get_name());
} else {