emacs: smarter error detection for quiet command.

Now quiet command can use the macro with-merlin-sync that synchronizes /after/ the point, lets you do your business, and report back to the user the errors concerning the phrases /before/ the current one.
emacs: C-down/C-up now are used to move around in the buffer or type typed tree after a type enclosing.
emacs: retract now drops the contents after the retracting point.
emacs: fixed typo in presenting module type when completing.