| Serhii Khoma | 5ca8f22 | 2024-11-12 21:49:42 +0100 | [diff] [blame] | 1 | " Vim syntax file |
| 2 | " Language: Idris 2 |
| 3 | " Maintainer: Idris Hackers (https://github.com/edwinb/idris2-vim), Serhii Khoma <srghma@gmail.com> |
| 4 | " Last Change: 2024 Nov 05 |
| 5 | " Original Author: raichoo (raichoo@googlemail.com) |
| 6 | " License: Vim (see :h license) |
| 7 | " Repository: https://github.com/ShinKage/idris2-nvim |
| 8 | " |
| 9 | |
| 10 | if exists("b:current_syntax") |
| 11 | finish |
| 12 | endif |
| 13 | |
| 14 | syn match idris2TypeDecl "[a-zA-Z][a-zA-z0-9_']*\s\+:\s\+" contains=idris2Identifier,idris2Operators |
| 15 | syn region idris2Parens matchgroup=idris2Delimiter start="(" end=")" contains=TOP,idris2TypeDecl |
| 16 | syn region idris2Brackets matchgroup=idris2Delimiter start="\[" end="]" contains=TOP,idris2TypeDecl |
| 17 | syn region idris2Block matchgroup=idris2Delimiter start="{" end="}" contains=TOP,idris2TypeDecl |
| 18 | syn region idris2SnocBrackets matchgroup=idris2Delimiter start="\[<" end="]" contains=TOP |
| 19 | syn region idris2ListBrackets matchgroup=idris2Delimiter start="\[>" end="]" contains=TOP |
| 20 | syn keyword idris2Module module namespace |
| 21 | syn keyword idris2Import import |
| 22 | syn keyword idris2Structure data record interface implementation |
| 23 | syn keyword idris2Where where |
| 24 | syn keyword idris2Visibility public abstract private export |
| 25 | syn keyword idris2Block parameters mutual using |
| 26 | syn keyword idris2Totality total partial covering |
| 27 | syn keyword idris2Annotation auto impossible default constructor |
| 28 | syn keyword idris2Statement do case of rewrite with proof |
| 29 | syn keyword idris2Let let in |
| 30 | syn keyword idris2Forall forall |
| 31 | syn keyword idris2DataOpt noHints uniqueSearch search external noNewtype containedin=idris2Brackets |
| 32 | syn keyword idris2Conditional if then else |
| 33 | syn match idris2Number "\<[0-9]\+\>\|\<0[xX][0-9a-fA-F]\+\>\|\<0[oO][0-7]\+\>" |
| 34 | syn match idris2Float "\<[0-9]\+\.[0-9]\+\([eE][-+]\=[0-9]\+\)\=\>" |
| 35 | syn match idris2Delimiter "[,;]" |
| 36 | syn keyword idris2Infix prefix infix infixl infixr |
| 37 | syn match idris2Operators "\([-!#$%&\*\+./<=>\?@\\^|~:]\|\<_\>\)" |
| 38 | syn match idris2Type "\<[A-Z][a-zA-Z0-9_']*\>" |
| 39 | syn keyword idris2Todo TODO FIXME XXX HACK contained |
| 40 | syn match idris2LineComment "---*\([^-!#$%&\*\+./<=>\?@\\^|~].*\)\?$" contains=idris2Todo,@Spell |
| 41 | syn match idris2DocComment "|||\([^-!#$%&\*\+./<=>\?@\\^|~].*\)\?$" contains=idris2Todo,@Spell |
| 42 | syn match idris2MetaVar "?[a-zA-Z_][A-Za-z0-9_']*" |
| 43 | syn match idris2Pragma "%\(hide\|logging\|auto_lazy\|unbound_implicits\|prefix_record_projections\|ambiguity_depth\|nf_metavar_threshold\|search_timeout\|pair\|rewrite\|integerLit\|stringLit\|charLit\|doubleLit\|name\|start\|allow_overloads\|language\|default\|transform\|hint\|globalhint\|defaulthint\|inline\|noinline\|extern\|macro\|spec\|foreign\|nomangle\|builtin\|MkWorld\|World\|search\|runElab\|tcinline\|auto_implicit_depth\)" |
| 44 | syn match idris2Char "'[^'\\]'\|'\\.'\|'\\u[0-9a-fA-F]\{4}'" |
| 45 | syn match idris2Backtick "`[A-Za-z][A-Za-z0-9_']*`" |
| 46 | syn region idris2String start=+"+ skip=+\\\\\|\\"+ end=+"+ contains=@Spell |
| 47 | syn region idris2BlockComment start="{-" end="-}" contains=idris2BlockComment,idris2Todo,@Spell |
| 48 | syn match idris2Identifier "[a-zA-Z][a-zA-z0-9_']*" contained |
| 49 | |
| 50 | " Default Highlighting {{{1 |
| 51 | |
| 52 | highlight def link idris2Deprecated Error |
| 53 | highlight def link idris2Identifier Identifier |
| 54 | highlight def link idris2Import Structure |
| 55 | highlight def link idris2Module Structure |
| 56 | highlight def link idris2Structure Structure |
| 57 | highlight def link idris2Statement Statement |
| 58 | highlight def link idris2Forall Structure |
| 59 | highlight def link idris2DataOpt Statement |
| 60 | highlight def link idris2DSL Statement |
| 61 | highlight def link idris2Block Statement |
| 62 | highlight def link idris2Annotation Statement |
| 63 | highlight def link idris2Where Structure |
| 64 | highlight def link idris2Let Structure |
| 65 | highlight def link idris2Totality Statement |
| 66 | highlight def link idris2Visibility Statement |
| 67 | highlight def link idris2Conditional Conditional |
| 68 | highlight def link idris2Pragma Statement |
| 69 | highlight def link idris2Number Number |
| 70 | highlight def link idris2Float Float |
| 71 | highlight def link idris2Delimiter Delimiter |
| 72 | highlight def link idris2Infix PreProc |
| 73 | highlight def link idris2Operators Operator |
| 74 | highlight def link idris2Type Include |
| 75 | highlight def link idris2DocComment Comment |
| 76 | highlight def link idris2LineComment Comment |
| 77 | highlight def link idris2BlockComment Comment |
| 78 | highlight def link idris2Todo Todo |
| 79 | highlight def link idris2MetaVar Macro |
| 80 | highlight def link idris2String String |
| 81 | highlight def link idris2Char String |
| 82 | highlight def link idris2Backtick Operator |
| 83 | |
| 84 | let b:current_syntax = "idris2" |
| 85 | |
| 86 | " vim: nowrap sw=2 sts=2 ts=8 noexpandtab ft=vim |