On 3/7/19 12:54 PM, Ciprian Dorin Craciun wrote:
> 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

Special characters in URLs are handled by percent-escaping:
vector->list as a fragment-identifier becomes #vector-%3Elist

It seems better to use use standard percent-escaping rather than
a custom encoding.

Using a fixed prefix may make sense, for example "proc:":

   <p id="proc:vector-list">

becomes a URL like:

   foo.html#proc%3Avector-%3Elist

The advantage of a prefix is that it can start with a letter (which satisfies the
recommendation in my link), and it avoid clashing with other anchors.  It may also
help with index generation.
--
	--Per Bothner
xxxxxx@bothner.com   http://per.bothner.com/