From b279d7b45cda89e2f019a0d3d0de9acaa7606547 Mon Sep 17 00:00:00 2001 From: Max Zinkus Date: Mon, 2 Dec 2019 16:34:22 -0500 Subject: [PATCH 1/2] Update syntax file to handle nested comments Addresses https://github.com/FStarLang/VimFStar/issues/17 This may introduce some weird edge cases with nested comments. However, it preserves correct behavior for normal comments and fixes the case of nested comments in a similar way to vim's `c.vim` (using a dedicated region for line comments). As with `c.vim`, we shrug at the edge cases. --- syntax/fstar.vim | 25 +++++++++++++------------ 1 file changed, 13 insertions(+), 12 deletions(-) diff --git a/syntax/fstar.vim b/syntax/fstar.vim index 95a3275..ffc9eb9 100644 --- a/syntax/fstar.vim +++ b/syntax/fstar.vim @@ -74,7 +74,7 @@ syn region fstarEncl transparent matchgroup=fstarKeyword start="\[|" matchgrou " Comments syn region fstarComment start="(\*" end="\*)" contains=@Spell,fstarComment,fstarTodo -syn match fstarComment "//.*$" contains=fstarComment,fstarTodo,@Spell +syn match fstarCommentLine "//.*$" contains=fstarComment,fstarCommentLine,fstarTodo,@Spell syn keyword fstarTodo contained TODO FIXME XXX NOTE @@ -105,33 +105,33 @@ syn region fstarNone matchgroup=fstarKeyword start="\" matchgroup=fstarKe " "sig" syn region fstarSig matchgroup=fstarModule start="\" matchgroup=fstarModule end="\" contains=ALLBUT,@fstarContained,fstarEndErr,fstarModule -syn region fstarModSpec matchgroup=fstarKeyword start="\" matchgroup=fstarModule end="\<\u\(\w\|'\)*\>" contained contains=@fstarAllErrs,fstarComment skipwhite skipempty nextgroup=fstarModTRWith,fstarMPRestr +syn region fstarModSpec matchgroup=fstarKeyword start="\" matchgroup=fstarModule end="\<\u\(\w\|'\)*\>" contained contains=@fstarAllErrs,fstarComment,fstarCommentLine skipwhite skipempty nextgroup=fstarModTRWith,fstarMPRestr " "open" -syn region fstarNone matchgroup=fstarKeyword start="\" matchgroup=fstarModule end="\<\u\(\w\|'\)*\( *\. *\u\(\w\|'\)*\)*\>" contains=@fstarAllErrs,fstarComment +syn region fstarNone matchgroup=fstarKeyword start="\" matchgroup=fstarModule end="\<\u\(\w\|'\)*\( *\. *\u\(\w\|'\)*\)*\>" contains=@fstarAllErrs,fstarComment,fstarCommentLine " "include" syn match fstarKeyword "\" skipwhite skipempty nextgroup=fstarModParam,fstarFullMod " "module" - somewhat complicated stuff ;-) -syn region fstarModule matchgroup=fstarKeyword start="\" matchgroup=fstarModule end="\<\u\(\w\|'\)*\>" contains=@fstarAllErrs,fstarComment skipwhite skipempty nextgroup=fstarPreDef -syn region fstarPreDef start="."me=e-1 matchgroup=fstarKeyword end="\l\|=\|)"me=e-1 contained contains=@fstarAllErrs,fstarComment,fstarModParam,fstarModTypeRestr,fstarModTRWith nextgroup=fstarModPreRHS +syn region fstarModule matchgroup=fstarKeyword start="\" matchgroup=fstarModule end="\<\u\(\w\|'\)*\>" 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 fstarModParam start="([^*]" end=")" contained contains=@fstarAENoParen,fstarModParam1,fstarVal syn match fstarModParam1 "\<\u\(\w\|'\)*\>" contained skipwhite skipempty nextgroup=fstarPreMPRestr -syn region fstarPreMPRestr start="."me=e-1 end=")"me=e-1 contained contains=@fstarAllErrs,fstarComment,fstarMPRestr,fstarModTypeRestr +syn region fstarPreMPRestr start="."me=e-1 end=")"me=e-1 contained contains=@fstarAllErrs,fstarComment,fstarCommentLine,fstarMPRestr,fstarModTypeRestr -syn region fstarMPRestr start=":" end="."me=e-1 contained contains=@fstarComment skipwhite skipempty nextgroup=fstarMPRestr1,fstarMPRestr2,fstarMPRestr3 +syn region fstarMPRestr start=":" end="."me=e-1 contained contains=@fstarComment,fstarCommentLine skipwhite skipempty nextgroup=fstarMPRestr1,fstarMPRestr2,fstarMPRestr3 syn region fstarMPRestr1 matchgroup=fstarModule start="\ssig\s\=" matchgroup=fstarModule end="\" contained contains=ALLBUT,@fstarContained,fstarEndErr,fstarModule -syn region fstarMPRestr2 start="\sfunctor\(\s\|(\)\="me=e-1 matchgroup=fstarKeyword end="->" contained contains=@fstarAllErrs,fstarComment,fstarModParam skipwhite skipempty nextgroup=fstarFuncWith,fstarMPRestr2 +syn region fstarMPRestr2 start="\sfunctor\(\s\|(\)\="me=e-1 matchgroup=fstarKeyword end="->" contained contains=@fstarAllErrs,fstarComment,fstarCommentLine,fstarModParam skipwhite skipempty nextgroup=fstarFuncWith,fstarMPRestr2 syn match fstarMPRestr3 "\w\(\w\|'\)*\( *\. *\w\(\w\|'\)*\)*" contained syn match fstarModPreRHS "=" contained skipwhite skipempty nextgroup=fstarModParam,fstarFullMod syn keyword fstarKeyword val -syn region fstarVal matchgroup=fstarKeyword start="\" matchgroup=fstarLCIdentifier end="\<\l\(\w\|'\)*\>" contains=@fstarAllErrs,fstarComment,fstarFullMod skipwhite skipempty nextgroup=fstarMPRestr -syn region fstarModRHS start="." end=". *\w\|([^*]"me=e-2 contained contains=fstarComment skipwhite skipempty nextgroup=fstarModParam,fstarFullMod +syn region fstarVal matchgroup=fstarKeyword start="\" matchgroup=fstarLCIdentifier end="\<\l\(\w\|'\)*\>" contains=@fstarAllErrs,fstarComment,fstarCommentLine,fstarFullMod skipwhite skipempty nextgroup=fstarMPRestr +syn region fstarModRHS start="." end=". *\w\|([^*]"me=e-2 contained contains=fstarComment,fstarCommentLine skipwhite skipempty nextgroup=fstarModParam,fstarFullMod syn match fstarFullMod "\<\u\(\w\|'\)*\( *\. *\u\(\w\|'\)*\)*" contained skipwhite skipempty nextgroup=fstarFuncWith -syn region fstarFuncWith start="([^*]"me=e-1 end=")" contained contains=fstarComment,fstarWith,fstarFuncStruct skipwhite skipempty nextgroup=fstarFuncWith +syn region fstarFuncWith start="([^*]"me=e-1 end=")" contained contains=fstarComment,fstarCommentLine,fstarWith,fstarFuncStruct skipwhite skipempty nextgroup=fstarFuncWith syn region fstarFuncStruct matchgroup=fstarModule start="[^a-zA-Z]struct\>"hs=s+1 matchgroup=fstarModule end="\" contains=ALLBUT,@fstarContained,fstarEndErr syn match fstarModTypeRestr "\<\w\(\w\|'\)*\( *\. *\w\(\w\|'\)*\)*\>" contained @@ -143,7 +143,7 @@ syn region fstarWithRest start="[^)]" end=")"me=e-1 contained contains=ALLBUT, syn region fstarStruct matchgroup=fstarModule start="\<\(module\s\+\)\=struct\>" matchgroup=fstarModule end="\" contains=ALLBUT,@fstarContained,fstarEndErr " "module type" -syn region fstarKeyword start="\\s*\\(\s*\\)\=" matchgroup=fstarModule end="\<\w\(\w\|'\)*\>" contains=fstarComment skipwhite skipempty nextgroup=fstarMTDef +syn region fstarKeyword start="\\s*\\(\s*\\)\=" matchgroup=fstarModule end="\<\w\(\w\|'\)*\>" contains=fstarComment,fstarCommentLine skipwhite skipempty nextgroup=fstarMTDef syn match fstarMTDef "=\s*\w\(\w\|'\)*\>"hs=s+1,me=s+1 skipwhite skipempty nextgroup=fstarFullMod syn keyword fstarKeyword and as assume assert @@ -276,6 +276,7 @@ if version >= 508 || !exists("did_fstar_syntax_inits") HiLink fstarErr Error HiLink fstarComment Comment + HiLink fstarCommentLine Comment HiLink fstarModPath Include HiLink fstarObject Include From a3a9e92b0d8473314007fde066fdee6ef1b1fe9d Mon Sep 17 00:00:00 2001 From: Max Zinkus Date: Mon, 2 Dec 2019 17:54:02 -0500 Subject: [PATCH 2/2] Fix module line syntax matching --- syntax/fstar.vim | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/syntax/fstar.vim b/syntax/fstar.vim index ffc9eb9..f01a3b1 100644 --- a/syntax/fstar.vim +++ b/syntax/fstar.vim @@ -114,7 +114,7 @@ syn region fstarNone matchgroup=fstarKeyword start="\" matchgroup=fstar syn match fstarKeyword "\" skipwhite skipempty nextgroup=fstarModParam,fstarFullMod " "module" - somewhat complicated stuff ;-) -syn region fstarModule matchgroup=fstarKeyword start="\" matchgroup=fstarModule end="\<\u\(\w\|'\)*\>" contains=@fstarAllErrs,fstarComment,fstarCommentLine skipwhite skipempty nextgroup=fstarPreDef +syn region fstarModule matchgroup=fstarKeyword start="\" 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 fstarModParam start="([^*]" end=")" contained contains=@fstarAENoParen,fstarModParam1,fstarVal syn match fstarModParam1 "\<\u\(\w\|'\)*\>" contained skipwhite skipempty nextgroup=fstarPreMPRestr