Manual: Add command names for agenda keys

This patch also defines a number of macros to typeset keys.  Too many,
maybe, because at first I wanted to be able to include all the
previous typesetting.  I think I will try to reduce the number
eventually - but for now this is it.