Closed lephe closed 2 years ago
👍
Finally, it recomputes the byte-based error ranges returned by CoqIDE so they match the character-based indexing of Sublime.
Ah, I didn't realize this was happening! Sure enough, Coq reports error ranges in bytes, not characters.
This PR adds
CoqError
regions to highlight errors in the code in split pane mode. It's identical to the way they're displayed in the inline view, I assume they were just missing.It also clears the error regions whenever the code is modified (similar to CoqIDE) because the indexing becomes incorrect after edits (and anyway the point of edits following an error is generally to fix it).
Finally, it recomputes the byte-based error ranges returned by CoqIDE so they match the character-based indexing of Sublime. Previously using Unicode notations would create issues. For instance, here the 3-byte character
≈
becomes a 3-character range, overflowing on nearby content:As another example, here each occurrence of the valid
≈
character in the command but before the error is counted for 3 bytes by CoqIDE but only counts as one character for Sublime, resulting in a 2-character shift to the right for every occurrence before the error (which is the first character of≈≈
):Both of these cases are now fixed. Note that because the high water mark is kept track of in character units, only Unicode characters within the command need to be re-counted, which allows a naive counting method without needing to fear performance issues.