Skip to content

Commit 5e9a68f

Browse files
committed
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.
1 parent 49c6f38 commit 5e9a68f

File tree

2 files changed

+24
-2
lines changed

2 files changed

+24
-2
lines changed

idris-commands.el

Lines changed: 17 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -502,7 +502,23 @@ Considered as a global variable"
502502

503503
(defun idris-eldoc-lookup ()
504504
"Return Eldoc string associated with the thing at point."
505-
(get-char-property (point) 'idris-eldoc))
505+
(let ((prop-val (get-char-property (point) 'idris-eldoc)))
506+
;; Idris2 temporary hack to make eldoc bit useful
507+
(if (and (stringp prop-val) (string-suffix-p ": " prop-val) (>=-protocol-version 2 1))
508+
(let* ((thing (idris-name-at-point))
509+
(ty (idris-eval (list :type-of thing) t))
510+
;; (ty (idris-eval (list :docs-for thing) t))
511+
(result (car ty))
512+
(formatting (cdr ty))
513+
(result-colour (idris-propertize-str (idris-repl-semantic-text-props formatting)
514+
result)))
515+
;; memoize result
516+
(dolist (overlay (overlays-at (point)))
517+
(when (overlay-get overlay 'idris-source-highlight)
518+
(overlay-put overlay 'idris-eldoc result-colour)))
519+
result-colour)
520+
;; Idris 1 using :doc-overview semantic properties extracted from highlights
521+
prop-val)))
506522

507523
(defun idris-pretty-print ()
508524
"Get a term or definition pretty-printed by Idris.

idris-common-utils.el

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -123,6 +123,13 @@ inserted text (that is, relative to point prior to insertion)."
123123
(+ ,start begin length)
124124
props))))))
125125

126+
(defun idris-propertize-str (spans text)
127+
"Add properties indicated by SPANS to the TEXT.
128+
SPANS is a list of (BEGIN LENGTH PROPERTIES) elements."
129+
(dolist (span spans text)
130+
(cl-destructuring-bind (begin length props) span
131+
(set-text-properties begin (+ begin length) props text))))
132+
126133
;;; TODO: Take care of circular dependency issue
127134
(autoload 'idris-eval "inferior-idris.el")
128135

@@ -224,7 +231,6 @@ inserted text (that is, relative to point prior to insertion)."
224231
(cadr namespace)))
225232
(t nil))))
226233

227-
228234
(defun idris-semantic-properties-help-echo (props)
229235
(let* ((name (assoc :name props))
230236
(decor (assoc :decor props))

0 commit comments

Comments
 (0)