search

FStarLang / fstar-mode.el

Emacs support for F*
Apache License 2.0
67 stars 17 forks source link

Undesirable comments with (// #42

Closed kyoDralliam closed 7 years ago

kyoDralliam commented 7 years ago

The characters (// seems to be interpreted by fstar-mode as a comment initiator which cannot be terminated (It displays everything until the end of buffer as commented).

cpitclaudel commented 7 years ago

Cute. Let me have a look :) (and thanks for spotting that!)

cpitclaudel commented 7 years ago

This is trickier than I expected (see http://lists.gnu.org/archive/html/emacs-devel/2017-01/msg00144.html for background).

I can think of a workaround, but I'd also like to know how pressing this is (given that there exists a reliable workaround of adding a space between the ( and the /). IOW, do you regularly run into this issue?

s-zanella commented 7 years ago

I've encountered this problem before and worked around it by restructuring the source (adding a space, moving the comment to other place), or switching to a (* ... *) style comment. It's a curious behaviour, but I'd consider a fix low priority since it's easy to work around.

cpitclaudel commented 7 years ago

Thanks for the feedback! It's certainly annoying (and surprising, too — I was expecting this to just stem from a typo, but it's actually a pretty deep Emacs issue)

kyoDralliam commented 7 years ago

Well it is sometimes produced by the new printer/reindenting tool that we would like to use automatically on fstar sources so it is a little annoying (of course I can add a space before each comments but I would prefer not doing so if possible).

cpitclaudel commented 7 years ago

Ok, I'll look into a fix.

cpitclaudel commented 7 years ago

Should be good; please confirm the fix when you have time :)

kyoDralliam commented 7 years ago

Yep, thank you very much