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