diff --git a/src/emacs/lean-debug.el b/src/emacs/lean-debug.el index 753c24065e..f5f455e9a4 100644 --- a/src/emacs/lean-debug.el +++ b/src/emacs/lean-debug.el @@ -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." diff --git a/src/shell/server.cpp b/src/shell/server.cpp index 10bd2b18e1..9c4afcb67f 100644 --- a/src/shell/server.cpp +++ b/src/shell/server.cpp @@ -277,8 +277,8 @@ json server::handle_complete(json const & req) { std::vector> 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 {