Skip to content

Commit

Permalink
Highlight Structure as a synonym for Record (whonore#357)
Browse files Browse the repository at this point in the history
  • Loading branch information
whonore authored and Rixxc committed Jul 2, 2024
1 parent 18631b1 commit c956b8c
Show file tree
Hide file tree
Showing 3 changed files with 8 additions and 6 deletions.
2 changes: 2 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,8 @@
(PR #339)

### Fixed
- Highlight `Structure` as a synonym for `Record`.
(PR #357)
- Don't try to decode partial JSON responses, avoiding a potential overflow
error in NeoVim for very long responses.
(PR #353)
Expand Down
6 changes: 3 additions & 3 deletions syntax/coq-infos.vim
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ syn case match
" Various
syn match coqVernacPunctuation ":=\|\.\|:"
syn match coqIdent contained "[[:digit:]']\@!\k\k*"
syn keyword coqTopLevel Declare Type Canonical Structure Cd Coercion Derive Drop Existential
syn keyword coqTopLevel Declare Type Canonical Cd Coercion Derive Drop Existential

" Binders
syn region coqBinder contained contains=coqIdent,coqBinderTypeParen matchgroup=coqVernacPunctuation start="(" end=")" keepend
Expand Down Expand Up @@ -114,8 +114,8 @@ syn region coqIndNotScope contained contains=coqIndBody matchgroup=coqVernacP
syn match coqConstructor contained "[[:digit:]']\@!\k\k*"

" Records
syn region coqRec contains=coqRecProfile start="\<Record\>" matchgroup=coqVernacPunctuation end="^\S"me=e-1 keepend
syn region coqRecProfile contained contains=coqIdent,coqRecTerm,coqBinder matchgroup=coqVernacCmd start="Record" matchgroup=NONE end="^\S"me=e-1
syn region coqRec contains=coqRecProfile start="\<Record\>\|\<Structure\>" matchgroup=coqVernacPunctuation end="^\S"me=e-1 keepend
syn region coqRecProfile contained contains=coqIdent,coqRecTerm,coqBinder matchgroup=coqVernacCmd start="Record\|Structure" matchgroup=NONE end="^\S"me=e-1
syn region coqRecTerm contained contains=@coqTerm,coqRecContent matchgroup=coqVernacPunctuation start=":" end="^\S"me=e-1
syn region coqRecContent contained contains=coqConstructor,coqRecStart matchgroup=coqVernacPunctuation start=":=" end="^\S"me=e-1
syn region coqRecStart contained contains=coqRecField,@coqTerm start="{" matchgroup=coqVernacPunctuation end="}" keepend
Expand Down
6 changes: 3 additions & 3 deletions syntax/coq.vim
Original file line number Diff line number Diff line change
Expand Up @@ -82,7 +82,7 @@ syn case match
syn match coqError "\S\+"
syn match coqVernacPunctuation ":=\|\.\|:"
syn match coqIdent contained "[[:digit:]']\@!\k\k*"
syn keyword coqTopLevel Type Structure Cd Drop Existential
syn keyword coqTopLevel Type Cd Drop Existential
"...
syn keyword coqVernacCmd Local Global Polymorphic Functional Scheme Back Combined
syn keyword coqVernacCmd Fail Succeed
Expand Down Expand Up @@ -414,8 +414,8 @@ syn region coqIndNotScope contained contains=coqIndBody matchgroup=coqVernacP
syn match coqConstructor contained "[[:digit:]']\@!\k\k*"

" Records
syn region coqRec contains=coqRecProfile start="\<Record\>" matchgroup=coqVernacPunctuation end="\.\_s" keepend
syn region coqRecProfile contained contains=coqIdent,coqRecTerm,coqBinder matchgroup=coqVernacCmd start="Record" matchgroup=NONE end="\.\_s"
syn region coqRec contains=coqRecProfile start="\<Record\>\|\<Structure\>" matchgroup=coqVernacPunctuation end="\.\_s" keepend
syn region coqRecProfile contained contains=coqIdent,coqRecTerm,coqBinder matchgroup=coqVernacCmd start="Record\|Structure" matchgroup=NONE end="\.\_s"
syn region coqRecTerm contained contains=@coqTerm,coqRecContent matchgroup=coqVernacPunctuation start=":" end="\.\_s"
syn region coqRecContent contained contains=coqConstructor,coqRecStart matchgroup=coqVernacPunctuation start=":=" end="\.\_s"
syn region coqRecStart contained contains=coqRecField,@coqTerm start="{" matchgroup=coqVernacPunctuation end="}" keepend
Expand Down

0 comments on commit c956b8c

Please sign in to comment.