[Agda] goal normalization request

[Darryl]

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. It would be incredibly useful if the focused goal showed up as un-normalized, and could be normalized, or possibly stepped, so that users can control how much normalization they see. This would be especially useful because it would eliminate the need for certain wrapper types that exist only to prevent normalization.

- darryl mcadams
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20121212/0546045b/attachment.html