diff --git a/src/emacs/lean-info.el b/src/emacs/lean-info.el index 6d2fcb3f3..01d62f6ad 100644 --- a/src/emacs/lean-info.el +++ b/src/emacs/lean-info.el @@ -655,6 +655,7 @@ Take out \"BEGININFO\" and \"ENDINFO\" and Use \"ACK\" as a delim." (defun lean-get-full-name-at-point-cont (info-record) "Continuation of lean-get-full-name-at-point" + (lean-server-debug "lean-get-full-name-at-point-cont: %S" info-record) (let ((id (cl-first (lean-info-record-identifier info-record)))) (when id (lean-info-identifier-body-str id)))) @@ -663,7 +664,7 @@ Take out \"BEGININFO\" and \"ENDINFO\" and Use \"ACK\" as a delim." "Return the full-name at point (if any)" (lean-get-info-record-at-point (lambda (info-record) - (lean-server-debug "executing continuation for get-full-name-at-point") + (lean-server-debug "lean-get-full-name-at-point: executing continuation for get-full-name-at-point") (funcall cont (lean-get-full-name-at-point-cont info-record))))) diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el index fab3cfe12..7f90baa7e 100644 --- a/src/emacs/lean-mode.el +++ b/src/emacs/lean-mode.el @@ -158,8 +158,7 @@ enabled and disabled respectively.") (when lean-eldoc-use (set (make-local-variable 'eldoc-documentation-function) 'lean-eldoc-documentation-function) - (eldoc-mode t) - (lean-eldoc-documentation-function)) + (eldoc-mode t)) ;; company-mode (when lean-company-use (company-lean-hook))) diff --git a/src/emacs/lean-server.el b/src/emacs/lean-server.el index a944895de..58f62ef2f 100644 --- a/src/emacs/lean-server.el +++ b/src/emacs/lean-server.el @@ -39,7 +39,8 @@ "Display a message at the bottom of the *lean-server* buffer." (lean-server-output-to-buffer (lean-server-get-buffer) (concat format-string) - args)) + args) + (apply 'lean-server-debug (cons format-string args))) (defun lean-server-trace (format-string &rest args) "Display a message at the bottom of the *lean-server* buffer." @@ -486,7 +487,9 @@ Otherwise, set an idle-timer to call the handler again" (lean-server-async-task-queue-pop-front) (lean-server-debug "event-handler: processed. now the queue size = %d\n" (lean-server-async-task-queue-len)) - ret))) + ret) + (t (lean-server-debug "event-handler: not processed. now the queue size = %d\n" + (lean-server-async-task-queue-len))))) (if lean-global-async-task-queue (lean-server-set-timer-for-event-handler)))) (defun lean-server-after-save () diff --git a/src/emacs/lean-tags.el b/src/emacs/lean-tags.el index 7489a327d..c2772a1fb 100644 --- a/src/emacs/lean-tags.el +++ b/src/emacs/lean-tags.el @@ -48,7 +48,11 @@ (interactive) (lean-get-full-name-at-point (lambda (full-name) - (when full-name (find-tag full-name))))) + (lean-server-debug "lean-find-tag: %s" full-name) + (when full-name + (condition-case err + (find-tag full-name) + (user-error (message "lean-find-tag error: %s" (cdr err)))))))) (defun lean-complete-tag () "complete with tag"