[css-highlight-api] should priority be a floating point number or an integer?

[frivoal]

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.

[hober]

If we use numbers at all for this, we should just match z-index and use integers.

[sanketj]

@frivoal @hober @fantasai I don't have strong opinions on this, but I'm in favor of keeping this simple and just using integers. Are you all okay with that?

[astearns]

Given that there is the escape hatch of running through the HighlightRegistry and changing all of the numbers to whatever you like, I am also in favor of integers

[frivoal]

I'd go with integers too, I think the downside of floats I listed in #4592 (comment) is just asking for trouble.

[sanketj]

Updated the spec in the PR above to model the priority attribute as an integer. Closing this issue.