This commit adds a `documentation` face to the builtin themes, used
to highlight common documentation syntaxes:
/**
* JavaDoc
*/
/*!
* QtDoc
*/
/// Inline documentation
## Inline documentation
The face is only an alias to the `comment` one for now.
Closes#1944
This commit allows using the <semicolon> expansion in commands, instead
of `\;`.
It makes commands look more elegant, and prevents new-comers from
falling into the trap of using <a-;> without escaping the semicolon.
