Skip to content

Commit 5895b10

Browse files
hrutvikmn200
authored andcommitted
[vim] Fix attribute highlighting for Definition and Triviality
Thanks to @ordinarymath for the bug report.
1 parent 0bf0b27 commit 5895b10

File tree

1 file changed

+4
-2
lines changed

1 file changed

+4
-2
lines changed

tools/editor-modes/vim/hol4script.vim

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -63,7 +63,9 @@ syn region HOLString start=/«/ end=/»/ contains=MLEscChar
6363
syn region HOLDefnStart
6464
\ matchgroup=MLKeyword start="^\<Definition\>"
6565
\ end=":"me=e-1
66-
\ contains=MLIdent nextgroup=HOLDefnEnd
66+
\ contains=MLIdent,HOLThmExtra
67+
\ nextgroup=HOLDefnEnd
68+
6769
syn match HOLQED /^\<End\>/
6870
syn region HOLDefnEnd
6971
\ matchgroup=MLKeyword start=":"
@@ -105,7 +107,7 @@ syn region HOLThmProofFold
105107
syn region HOLTriviality
106108
\ matchgroup=MLKeyword start="^\<Triviality\>"
107109
\ end="[:=]"me=e-1
108-
\ contains=MLIdent
110+
\ contains=MLIdent,HOLThmExtra
109111
\ nextgroup=HOLThmProof
110112

111113
" (Co)Inductive

0 commit comments

Comments
 (0)