switching to absolute positions in the current buffer

[nikswamy]

Hi Clement,

First off: This is a very naive implementation. I don't expect you to accept this pull request as is.

Rather, it's a starting point for me to learn about fstar-mode.el and to make some changes to it corresponding to some upcoming changes in F*.

Basically, F* now reports errors of the form source-range: (Error) "some error message" (see source-range)

The first source-range is a range (typically in the current overlay) that contains some error. The second source-range is another range somewhere else in the program (perhaps in the current overlay, elsewhere in the current buffer, or in another file altogether) that reveals more information about the current error.

To support this, I started by changing fstar-mode.el to make use of absolute position information within the current buffer, rather than translating things relative to the current overlay using fstar-subp-adjust-line-numbers.

I'd be delighted to hear your thoughts about how best to indicate the related, second source-range reported in the message to the user. For example, currently, if the user navigates to the highlighted error location, we show the associated error message at the bottom. Perhaps at that point, if presses some key combination, we could jump to related source-range reported in the message? Any tips for how to implement something like that (or some other scheme that you think may be more appropriate) would be very helpful too.

Many thanks! -Nik

[cpitclaudel]

Hey Nik,

Sorry for the delay! This looks pretty good to me, actually. I'll leave comments in the diff.

Some questions regarding displaying related information:

• How large do you expect the second range to be? A few lines at most? Or could it be more?
• Will there ever be more than one error at a time? More than one per line?

Your idea sounds good (and easy to implement, too :). Here are another few options that we might consider in addition to jumping:

• Displaying an inline pop-up showing the related span in question.
• Showing a small button which, once activated, would jump to the related error (and another button to take you back)

A concrete example of such an error-location pair would be useful, too :)

[cpitclaudel]

All done :) Is there a reason for the F* subprocess to take line and column numbers, instead of just absolute offsets in the file?

Another thing that might be worth considering: using absolute offset makes it tricky to allow edition of comments or spaces without invalidating the corresponding region of the file. Not sure whether this matters, though (one could imagine caching on the F* side that would make reprocessing the unchanged code very fast).