FStarLang / VimFStar

A Vim mode for FStar
Vim License
24 stars 12 forks source link

Fix two syntax file issues #20

Closed maxzinkus closed 1 year ago

maxzinkus commented 4 years ago
  1. Nested comments, fixes #17
  2. Module line, fixes #19
maxzinkus commented 2 years ago

@mlr-msft 🙂

maxzinkus commented 1 year ago

@mlr-msft @SimonForest @fmrl @nikswamy @msprotz @protz anyone want to close this out so I can delete my fork? 🙏

mtzguido commented 1 year ago

Hello Max, thanks for this. The first commit looks good to me and fixes an old problem. The second one introduces a slight problem though, module paths have their last character not highlighted:

image

I was actually agreeing with your comment here https://github.com/FStarLang/VimFStar/issues/19#issuecomment-560786935, maybe like this? (remove the me=e-1, allow . in module names, change start of fstarPreDef to [:print:])

diff --git a/syntax/fstar.vim b/syntax/fstar.vim
index f01a3b1..2e607cd 100644
--- a/syntax/fstar.vim
+++ b/syntax/fstar.vim
@@ -114,8 +114,8 @@ syn region   fstarNone matchgroup=fstarKeyword start="\<open\>" matchgroup=fstar
 syn match    fstarKeyword "\<include\>" skipwhite skipempty nextgroup=fstarModParam,fstarFullMod

 " "module" - somewhat complicated stuff ;-)
-syn region   fstarModule matchgroup=fstarKeyword start="\<module\>" matchgroup=fstarModule end="\<\u\(\w\|'\)*\>"me=e-1 contains=@fstarAllErrs,fstarComment,fstarCommentLine skipwhite skipempty nextgroup=fstarPreDef
-syn region   fstarPreDef start="."me=e-1 matchgroup=fstarKeyword end="\l\|=\|)"me=e-1 contained contains=@fstarAllErrs,fstarComment,fstarCommentLine,fstarModParam,fstarModTypeRestr,fstarModTRWith nextgroup=fstarModPreRHS
+syn region   fstarModule matchgroup=fstarKeyword start="\<module\>" matchgroup=fstarModule end="\<\u\(\w\|\.\)*\>" contains=@fstarAllErrs,fstarComment,fstarCommentLine skipwhite skipempty nextgroup=fstarPreDef
+syn region   fstarPreDef start="[:print:]"me=e-1 matchgroup=fstarKeyword end="\l\|=\|)"me=e-1 contained contains=@fstarAllErrs,fstarComment,fstarCommentLine,fstarModParam,fstarModTypeRestr,fstarModTRWith nextgroup=fstarModPreRHS
 syn region   fstarModParam start="([^*]" end=")" contained contains=@fstarAENoParen,fstarModParam1,fstarVal
 syn match    fstarModParam1 "\<\u\(\w\|'\)*\>" contained skipwhite skipempty nextgroup=fstarPreMPRestr

That said I'm pretty unfamiliar with these files, so take with a grain of salt.

By the way, we are developing a VSCode extension for F*, so I doubt this repo will see much use. I however do have this installed for syntax highlighting, but I do not use the interactive mode.

maxzinkus commented 1 year ago

Ah! Irksome. If you want to snag that first commit in and omit the second, then that's totally fine by me. I've actually not looked at FStar with Vim in a while either 😅

Either way- thanks for following up!

mtzguido commented 1 year ago

Thanks, I pushed your first commit, and my edit of the second mentioning you.