fstar-mode.el icon indicating copy to clipboard operation
fstar-mode.el copied to clipboard

Published 20 hours ago • verified publisher icon FStarLang

c-c c-r reload better description

Open briangmilnes opened this issue 1 year ago • 3 comments

You could add the following to c-c c-r's documentation

F* parses your file on open and finds it's dependencies. If you add and 'open FStar.module' you need to reload the buffer with this command.

briangmilnes avatar Mar 22 '23 18:03 briangmilnes

Can you make a pull request?

cpitclaudel avatar Mar 23 '23 06:03 cpitclaudel

(Although I doubt that someone who doesn't yet know of this gotcha would know of C-c C-r, so I'm not sure it would help)

cpitclaudel avatar Mar 23 '23 06:03 cpitclaudel

Clement,

Thanks.

BTW, [@@@ ... ] does not work on a reload either. Makes the interface a bit choppy for a newb like myself.

Thanks, Brian

On Wed, Mar 22, 2023 at 11:21 PM Clément Pit-Claudel < @.***> wrote:

(Although I doubt that someone who doesn't yet know of this gotcha would know of C-c C-r, so I'm not sure it would help)

— Reply to this email directly, view it on GitHub https://github.com/FStarLang/fstar-mode.el/issues/133#issuecomment-1480658980, or unsubscribe https://github.com/notifications/unsubscribe-auth/ACKMDK6LMA57Q46KOHLDBDDW5PTVFANCNFSM6AAAAAAWEFXLOU . You are receiving this because you authored the thread.Message ID: @.***>

briangmilnes avatar Mar 23 '23 16:03 briangmilnes