search

agda / cornelis

agda-mode for neovim
BSD 3-Clause "New" or "Revised" License
135 stars 23 forks source link

Can't find interaction point 0 #133

Open JonathanLorimer opened 11 months ago

JonathanLorimer commented 11 months ago

Getting the error Can't find interaction point 0 when I run CornelisRefine

JonathanLorimer commented 11 months ago

Seems to be coming from here

JonathanLorimer commented 11 months ago

I think it might be an issue with concurrency, and when the interaction point gets inserted in to the interaction points map in BufferStuff:

data BufferStuff = BufferStuff
  { bs_agda_proc  :: Agda
  , bs_ips        :: Map InteractionId (InteractionPoint Identity)
  , bs_ip_exts    :: Map InteractionId Extmark
  , bs_goto_sites :: Map Extmark DefinitionSite
  , bs_goals      :: DisplayInfo
  , bs_info_win   :: InfoBuffer
  , bs_code_map   :: LineIntervals
  }
  deriving Generic
JonathanLorimer commented 11 months ago

It also may be that the interaction point state is getting clobbered somehow? If I do CornelisLoad and then CornelisRefine immediately before CornelisLoad has finished, refine seems to work (kind of like buffering a jump in a video game lol)