[Agda] Devel: How to get back normalisation instead of simplification?

[Wolfram Kahl]

On Sun, Jun 23, 2013 at 10:28:50PM -0400, Wolfram Kahl wrote:
> On Sat, Jun 22, 2013 at 08:27:20PM +0200, Andreas Abel wrote:
> > if you have some large terms in you developments and have not pulled 
> > Agda recently, it might be worth trying.  I have implemented some 
> > performance improvements that are probably noticeable if you use records 
> > a lot.  The relevant patches concern "issue 854".
> > 
> > James reported a reduction of memory consumption from 12GB to 3GB for 
> > one of his developments.
> > 
> > In case you see similar improvements, please reply to this message.
> 
> Wonderful!

... so I switched to the current development version.

But now the following gets in the way:

 | Mon May 20 06:33:15 EDT 2013  Andreas Abel <andreas.abel at ifi.lmu.de>
 |   * Switched to simplification (instead of normalisation) in emacs interaction.
 |   This is for experimentation purposes.
 |   Key-bindings for full normalisation should also be added.

Since there is already a distinction achieved via C-u
in the display of goals and context (see
  http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.EmacsModeKeyCombinations  
), perhaps it would be natural to expand on that,
making that distinction ternary instead of the current binary,
by adding simplified version via a special C-u prefix?

(In Emacs , C-u in general serves to pass a |just| argument of type
 |Maybe Integer| to the following command;
 just C-u without a numeric argument seems to pass |just 4|).

Otherwise, is there a simple way to switch back to full normalisation
as one of the options?


Wolfram