idris-hackers/idris-mode — pull request #81 by david-christiansen (2014-02-13 08:00:09+00:00)
Title: Highlighting and help tooltips for notes buffer

Now, a mouseover shows the available mouse commands and the region in
which they are available