Generated element IDs not unique

[eigengrau]

Headline element IDs are currently a function of the headline text. A document may contain several headlines with identical text (e.g. »More Information« across multiple sections of a document). This will then lead to non-unique element IDs, invalidating the HTML output and breaking jump-to-anchor functionality in browsers.