--- Day changed Sun Apr 02 2017
christiansenakr[m], mietek, adamse: it's pretty easy to add right-click menus in Emacs02/04 17:17
christiansenI wrote a little elisp library for idris-mode that can compute menus from the various bits of annotation at some location, perhaps it would be useful for agda-mode too02/04 17:17
mietekI think the #1 thing that would be useful for agda-mode is better goal display02/04 17:18
christiansenhttps://github.com/david-christiansen/prop-menu-el02/04 17:18
christiansenyeah, tooltips and colors and such would be nice there02/04 17:18
mieteksuch luxuries02/04 17:19
christiansenin Idris's equivalent, there's a right-click menu with things like "normalize" and "hide/show implicits"02/04 17:19
christiansenthat would be good too02/04 17:19
mietekhttps://github.com/agda/agda/issues/958#issuecomment-12902683802/04 17:20
mietekhttps://github.com/agda/agda/issues/63202/04 17:20
mietekfirst, let’s make it correct02/04 17:21
mietekthen, maybe sort things in a sane order02/04 17:21

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!