Assuming we continue having numerical priorities (see #4591), should the highlight priority be an integer instead of a double?

Downside of integers: likely to be used like BASIC line numbers, counting in 10s (or in 100s) to make insertion between two layers easy. Workable, but clumsy.

Downside of doubles: depending on the internal precision used to store these, in some browsers two very close numbers could be considered equal, while in other browsers they would be different. Depending on the order of insertion into CSS.highlights, this could result in the opposite ordering, and therefore interop problems.