fstar-jump-to-definition on a module should jump to the fsti if it exists

FStarLang / fstar-mode.el

Emacs support for F*

Apache License 2.0

67 stars 17 forks source link

fstar-jump-to-definition on a module should jump to the fsti if it exists #107

Open jaybosamiya opened 5 years ago

jaybosamiya commented 5 years ago

Currently, M-. (fstar-jump-to-definition) jumps to the fst of the module, when we do it over an open ModuleName, even if an fsti exists. I think it would be better if it were to jump over to the fsti and rely on a user to press C-c C-a (fstar-visit-interface-or-implementation) if need be to jump over to the implementation.

Not sure if this is something that needs to be fixed on the compiler side or on the fstar-mode side, but it would be a nice QoL improvement.

cpitclaudel commented 5 years ago

I think this is F* side; we just jump to the position it reports. But we could work around it on our side if needed. Here's I'd go about it (I don't have time to dive into it myself atm, but I think you could give it a try):

Turn debugging on.
Do a jump to definition
Look at what F* returns; I don't recall if it's easily distinguishable from a usual jump to a specific definition (in fact, this might even be special-cased in fstar-mode to jump directly to a file)
Find the corresponding bit in fstar-mode (ask me for help if this part is tricky)
Change it to test if an fsti is present and jump there if so

I would predicate the last part on a setting, but I wouldn't object to making jumping to the fsti the default.