This PR attaches extmarks to interaction points, and looks them up at runtime to determine a goal's interval. This fixes a bunch of weird bugs where the buffer would have changed and we'd compute the wrong thing to replace. Additionally, it gets rid of a BIG HACK, which is always nice.
Agda sends intervals that span interaction points, which we were using as the source of truth for where goals actually are in the document. But there's a better way: extmarks! Extmarks are attached to the buffer when we do syntax highlighting, and track changes to the document when we do edits. Therefore, the intervals spanned by extmarks are a much better source of truth than the intervals that come from Agda. As a bonus, we don't need to do any logic to try to keep the two in sync.
Unfortunately life isn't quite as easy as all of that; there's a delay between getting the goals and getting the highlighting, so we need to use the Agda-provided locations as a fallback in case we don't yet have an extmark.
This PR attaches extmarks to interaction points, and looks them up at runtime to determine a goal's interval. This fixes a bunch of weird bugs where the buffer would have changed and we'd compute the wrong thing to replace. Additionally, it gets rid of a BIG HACK, which is always nice.
Agda sends intervals that span interaction points, which we were using as the source of truth for where goals actually are in the document. But there's a better way: extmarks! Extmarks are attached to the buffer when we do syntax highlighting, and track changes to the document when we do edits. Therefore, the intervals spanned by extmarks are a much better source of truth than the intervals that come from Agda. As a bonus, we don't need to do any logic to try to keep the two in sync.
Unfortunately life isn't quite as easy as all of that; there's a delay between getting the goals and getting the highlighting, so we need to use the Agda-provided locations as a fallback in case we don't yet have an extmark.