plt-amy / agda Goto Github PK

I think the proper way to implement type-on-hover, context-at-point (outside of interaction points..) isn't to make the type checker yell every single term that it produces (that would take a billion trillion times more space than the interface files currently do), but to add a Note-or-something constructor to Term:

data Term
  = ...
  | Note Range Term

Then making sure that we serialize these ranges. This shouldn't increase the size of the interface files too much; it would allow us to cache this info; and every function that deals with terms (except for instantiateFull, since that runs on all definitions before serialization) could just strip off the Note constructors. We can then compute the RangeMap of Term that we need for hover information by first finding the clause that encloses the point, then inverting that.