On Thu, Mar 7, 2019 at 10:29 PM Per Bothner <xxxxxx@bothner.com> wrote:
> On 3/7/19 12:25 PM, Ciprian Dorin Craciun wrote:
> > Unfortunately the `id` and `href` attribute doesn't allow for such characters.
>
> Actually, they're allowed by HTML5, which only prohibits whitespace.
>
> https://developer.mozilla.org/en-US/docs/Web/HTML/Global_attributes/id

I was not aware of that (the HTML4 validator complained), however
given that some of these ID's will be put in HTTP API calls (or even
file-names if we want to extract sections as separate files), then I
think they should be kept as "safe" as possible, without requiring
much escaping.

Ciprian.