HTML: Generator does not check if HTML ids are unique

[mikir]

Currently, HTML generator does not check if generated HTML ids are unique.

Because HTML ids can be generated automatically from Markdown documentation comments (headings), such clashes can easily happen.

HTML generator should at least detect such HTML ids clashes or even better it could solve these clashes automatically.