From d85eff910823b795c82f86e44554a55881b70151 Mon Sep 17 00:00:00 2001 From: Marek L Date: Sat, 15 Jun 2024 00:18:28 +0100 Subject: [PATCH] Add fallback for Idris2 to use :type-of for eldoc-lookup Why: Idris2 IDE mode is lacking implementation of `doc-overview` attribute used in Idris 1 to display the short doc in minibuffer. This may be temporary until Idris2 implementation is updated. --- idris-commands.el | 18 +++++++++++++++++- idris-common-utils.el | 8 +++++++- 2 files changed, 24 insertions(+), 2 deletions(-) diff --git a/idris-commands.el b/idris-commands.el index 417c827..a468cd6 100644 --- a/idris-commands.el +++ b/idris-commands.el @@ -502,7 +502,23 @@ Considered as a global variable" (defun idris-eldoc-lookup () "Return Eldoc string associated with the thing at point." - (get-char-property (point) 'idris-eldoc)) + (let ((prop-val (get-char-property (point) 'idris-eldoc))) + ;; Idris2 temporary hack to make eldoc bit useful + (if (and (stringp prop-val) (string-suffix-p ": " prop-val) (>=-protocol-version 2 1)) + (let* ((thing (idris-name-at-point)) + (ty (idris-eval (list :type-of thing) t)) + ;; (ty (idris-eval (list :docs-for thing) t)) + (result (car ty)) + (formatting (cdr ty)) + (result-colour (idris-propertize-str (idris-repl-semantic-text-props formatting) + result))) + ;; memoize result + (dolist (overlay (overlays-at (point))) + (when (overlay-get overlay 'idris-source-highlight) + (overlay-put overlay 'idris-eldoc result-colour))) + result-colour) + ;; Idris 1 using :doc-overview semantic properties extracted from highlights + prop-val))) (defun idris-pretty-print () "Get a term or definition pretty-printed by Idris. diff --git a/idris-common-utils.el b/idris-common-utils.el index 3b8b803..44dbe8a 100644 --- a/idris-common-utils.el +++ b/idris-common-utils.el @@ -123,6 +123,13 @@ inserted text (that is, relative to point prior to insertion)." (+ ,start begin length) props)))))) +(defun idris-propertize-str (spans text) + "Add properties indicated by SPANS to the TEXT. +SPANS is a list of (BEGIN LENGTH PROPERTIES) elements." + (dolist (span spans text) + (cl-destructuring-bind (begin length props) span + (set-text-properties begin (+ begin length) props text)))) + ;;; TODO: Take care of circular dependency issue (autoload 'idris-eval "inferior-idris.el") @@ -224,7 +231,6 @@ inserted text (that is, relative to point prior to insertion)." (cadr namespace))) (t nil)))) - (defun idris-semantic-properties-help-echo (props) (let* ((name (assoc :name props)) (decor (assoc :decor props))