get "No goal at cursor" when there is one

[jakio6]

step to reproduce.

1. with this file
2. uncomment refl-counterexample
3. :CornelisLoad
4. change refl-example = refl to refl-example = ?
5. :CornelisLoad
6. :CornelisTypeContext at the ? added above
   • get "No goal at cursor"
7. repeat 5 and 6, not get the same message.

agda --version used:

Agda version 2.6.4.1
Built with flags (cabal -f)
 - enable-cluster-counting: unicode cluster counting in LaTeX backend using the ICU library
 - optimise-heavily: extra optimisations

I did a little debugging, it shows that I was getting a wrong extmark (doesn't match the cursor position) at step 6.

Here bs_ips might be used before it was updated?

cornelis/src/Lib.hs

Line 92 in 41b7d5e

& #bs_ip_exts <>~ M.compose extmap (fmap ip_interval' $ bs_ips bs)

Looks like the interaction points was updated in parallel with the routine above.

Works fine if I always do :CornelisLoad twice though.