Open LukeXuan opened 1 year ago
Hi Luke!
I don't know whether the "go to this exact point" behavior is still useful, but I suspect it is: the automatic logic to figure out where a block ends is not very good, and so it's good to be able to override it.
That said, I agree with you that I prefer your behavior when it works.
Doesn't C-c C-n do what you want in most cases? (Process the next block?)
Yes, C-c C-n
technically do the same thing, but I prefer C-c RET
for three reasons,
C-c RET
for years from coq-mode
has trained me to that binding only,C-c RET
can both retract and advance, while I would need to hit C-p
for retract otherwise.J/F
for me. As you can imagine, none of J-c J-n
, J-c F-n
or F-c F-n
is easy to work with.Maybe we could have a setting for this. Or maybe one of the F* devs can comment?
Being able to configure C-c C-RET to behave like C-c C-n sounds like a good idea to me.
FWIW, finding the end of the current definition is difficult without actually using F to parse the contents of the buffer. FYI, in fstar-vscode-assistant, when the user hits Ctrl+. the editor passes the current cursor location to the F server, F* parses the buffer and advances to checker to up to the definition that encloses the current cursor location.
FYI, in fstar-vscode-assistant, when the user hits Ctrl+. the editor passes the current cursor location to the F server, F parses the buffer and advances to checker to up to the definition that encloses the current cursor location.
It feels like the proper way to address the problem. Is it an API that emacs can also use or limited to vscode?
Is fstar-vscode-assistant using LSP or the custom F* protocol?
This pull request modifies the behavior of
fstar-subp-advance-or-retract-to-point
such that it will advance to the end of the current block.Previously, if the cursor is in the middle of a block, for example,
Pressing
C-c RET
will passlet foo(
to the sub-process, and reports an error. The updated function will pass the entirety oflet foo ...
to the process and succeed. This is helpful when I'm still trying to figure out the function body (especially if it spans multiple line), since I won't need to move my cursor (which I can useM-n
) and back (which is more difficult).I'm not a fstar power user and in all my use cases, I'm always advancing the proof checker on a block granularity. Maybe there is indeed a demand for sub-block advancement (maybe at tactic level, such as in Coq). If that's the case, I can create a separate function for this altered behavior and register a different key for it.