On 2012-12-12 19:28, Darryl wrote: > In emacs, goals don't normalize when they're all being displayed at > once (i.e. when no goal is currently in focus), but when one is in > focus, it only shows up normalized. Not necessarily: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.EmacsModeKeyCombinations -- /NAD