#248 doctools - Gather markup statistics

[Andreas Kupries]

Extend engine to gather statistics about the use of markup commands in a set of documents, and print them. Both only on demand.

Note: To get the actual commands used (i.e. deprecated ones) this has to be done in the syntax checking layer. Backend is too late, it sees only the canonical commands, and some are filtered out already (include, comments, ...)