idris-lang/Idris-dev — pull request #1525 by bmsherman (2014-09-15 04:55:30+00:00)
Title: Add annotations for :search result classification

This adds "doc-overview" annotation strings for the `>`, `<`, and `=` symbols that are returned for each search result in the :search feature. I also just added a [page to the Wiki which describes :search results in more detail](https://github.com/idris-lang/Idris-dev/wiki/Type-directed-search-(:search)).

These annotations currently do not display by default in Idris-mode, because there is no corresponding "name" annotation. I suggest that a change is made to "idris-mode" to support mouse hover text even when there is just "doc-overview" but no "name".