HTML "fixed" ids

[Rob Beezer]

Mitch got me going on allowed characters for @label attributes, and I could not
help noticing some stale code about "fixed ids" in HTML output.

Example: if you set @xml:id or @label to "ptx-masthead", then it will interfere
with a *fixed* HTML @id that we set to "ptx-masthead" for UI purposes.

Unlikely, but we treat these as fatal errors, since who knows what bad things
might happen?

The old list of eight or so banned strings has been replace by a new list of
about thirty strings.

So:

* We might see authors getting new error messages (@label, or fixed ids). Not
putting this on pretext-announce, so watch -support.

* JS authors need to be aware of this list and should help maintain it, rather
than a gross replacement like I just did. If somebody knows a good mechanism
for this, I'd be interested.

* Prefixing ids with "ptx-" is a great convention to help minimize the
likelihood of a collision. It has not been universally adopted.