Slightly improved indexing for the string-% operator, thanks to comments

from Skip Montanaro.  There is one weirdness in the final index for HTML, but
that is low priority.