Open briangmilnes opened 1 year ago
Does C-c ! C-c fstar work for this?
Clement,
It just says "cannot use syntax checker fstar in this buffer".
Interesting you'd ask, Brian
On Mon, Mar 20, 2023 at 4:02 PM Clément Pit-Claudel < @.***> wrote:
Does C-c ! C-c fstar work for this?
— Reply to this email directly, view it on GitHub https://github.com/FStarLang/fstar-mode.el/issues/129#issuecomment-1477061391, or unsubscribe https://github.com/notifications/unsubscribe-auth/ACKMDK3PM3X63DPZAD3232TW5DOWRANCNFSM6AAAAAAV7UD2RY . You are receiving this because you authored the thread.Message ID: @.***>
Ah, right because it's using the server. That's a bit annoying. Then I agree, it would be good to offer to save the buffer.
Clement,
Shall I fix it for you?
Thanks, Brian
On Fri, Mar 24, 2023, 12:07 AM Clément Pit-Claudel @.***> wrote:
Ah, right because it's using the server. That's a bit annoying. Then I agree, it would be good to offer to save the buffer.
— Reply to this email directly, view it on GitHub https://github.com/FStarLang/fstar-mode.el/issues/129#issuecomment-1482349594, or unsubscribe https://github.com/notifications/unsubscribe-auth/ACKMDK3JYKAG2LZLXS2LWGDW5VB3BANCNFSM6AAAAAAV7UD2RY . You are receiving this because you authored the thread.Message ID: @.***>
Well, it wouldn't be for me (I don't use F* these days), but if you want to write the patch, that would be great!
When you want to verify on the command line, fstar-mode should check if the current buffer is saved and do a save current file ask of the user.