2020-05-19 11:32:37 -04:00
|
|
|
" syntax highlighting for Idris 2 (idris-lang.org)
|
2020-02-22 15:32:56 -05:00
|
|
|
"
|
|
|
|
" Heavily modified version of the haskell syntax
|
2020-05-19 11:32:37 -04:00
|
|
|
" highlighter to support Idris 2.
|
2020-02-22 15:32:56 -05:00
|
|
|
"
|
|
|
|
" author: raichoo (raichoo@googlemail.com)
|
|
|
|
|
|
|
|
if exists("b:current_syntax")
|
|
|
|
finish
|
|
|
|
endif
|
|
|
|
|
|
|
|
syn match idrisTypeDecl "[a-zA-Z][a-zA-z0-9_']*\s\+:\s\+"
|
|
|
|
\ contains=idrisIdentifier,idrisOperators
|
|
|
|
syn region idrisParens matchgroup=idrisDelimiter start="(" end=")" contains=TOP,idrisTypeDecl
|
|
|
|
syn region idrisBrackets matchgroup=idrisDelimiter start="\[" end="]" contains=TOP,idrisTypeDecl
|
2021-12-28 03:56:16 -05:00
|
|
|
syn region idrisBrace matchgroup=idrisDelimiter start="{" end="}" contains=TOP,idrisTypeDecl
|
2021-12-28 03:56:16 -05:00
|
|
|
syn region idrisIdiom matchgroup=idrisDelimiter start="\[|" end="|]" contains=TOP,idrisTypeDecl
|
2020-02-22 15:32:56 -05:00
|
|
|
syn keyword idrisModule module namespace
|
|
|
|
syn keyword idrisImport import
|
2020-05-19 14:40:40 -04:00
|
|
|
syn keyword idrisStructure data record interface implementation
|
2020-02-22 15:32:56 -05:00
|
|
|
syn keyword idrisWhere where
|
|
|
|
syn keyword idrisVisibility public abstract private export
|
2020-05-19 14:40:40 -04:00
|
|
|
syn keyword idrisBlock parameters mutual using
|
2020-02-22 15:32:56 -05:00
|
|
|
syn keyword idrisTotality total partial covering
|
2020-05-19 14:40:40 -04:00
|
|
|
syn keyword idrisAnnotation auto impossible default constructor
|
|
|
|
syn keyword idrisStatement do case of rewrite with
|
2020-02-22 15:32:56 -05:00
|
|
|
syn keyword idrisLet let in
|
2020-05-19 14:40:40 -04:00
|
|
|
syn keyword idrisForall forall
|
|
|
|
syn keyword idrisDataOpt noHints uniqueSearch search external noNewtype containedin=idrisBrackets
|
2020-02-22 15:32:56 -05:00
|
|
|
syn keyword idrisConditional if then else
|
|
|
|
syn match idrisNumber "\<[0-9]\+\>\|\<0[xX][0-9a-fA-F]\+\>\|\<0[oO][0-7]\+\>"
|
|
|
|
syn match idrisFloat "\<[0-9]\+\.[0-9]\+\([eE][-+]\=[0-9]\+\)\=\>"
|
|
|
|
syn match idrisDelimiter "[,;]"
|
|
|
|
syn keyword idrisInfix prefix infix infixl infixr
|
|
|
|
syn match idrisOperators "\([-!#$%&\*\+./<=>\?@\\^|~:]\|\<_\>\)"
|
|
|
|
syn match idrisType "\<[A-Z][a-zA-Z0-9_']*\>"
|
|
|
|
syn keyword idrisTodo TODO FIXME XXX HACK contained
|
|
|
|
syn match idrisLineComment "---*\([^-!#$%&\*\+./<=>\?@\\^|~].*\)\?$" contains=idrisTodo,@Spell
|
|
|
|
syn match idrisDocComment "|||\([^-!#$%&\*\+./<=>\?@\\^|~].*\)\?$" contains=idrisTodo,@Spell
|
|
|
|
syn match idrisMetaVar "?[a-z][A-Za-z0-9_']*"
|
2021-12-30 07:51:17 -05:00
|
|
|
syn match idrisPragma "%\(hide\|logging\|auto_lazy\|unbound_implicits\|undotted_record_projections\|ambiguity_depth\|pair\|rewrite\|integerLit\|stringLit\|charLit\|name\|start\|allow_overloads\|language\|default\|transform\|hint\|global_hint\|defaulthint\|inline\|extern\|macro\|spec\|foreign\|runElab\|tcinline\|auto_implicit_depth\|builtin\)\>"
|
2020-02-22 15:32:56 -05:00
|
|
|
syn match idrisChar "'[^'\\]'\|'\\.'\|'\\u[0-9a-fA-F]\{4}'"
|
|
|
|
syn match idrisBacktick "`[A-Za-z][A-Za-z0-9_']*`"
|
|
|
|
syn region idrisString start=+"+ skip=+\\\\\|\\"+ end=+"+ contains=@Spell
|
|
|
|
syn region idrisBlockComment start="{-" end="-}" contains=idrisBlockComment,idrisTodo,@Spell
|
|
|
|
syn match idrisIdentifier "[a-zA-Z][a-zA-z0-9_']*" contained
|
|
|
|
|
|
|
|
highlight def link idrisDeprecated Error
|
|
|
|
highlight def link idrisIdentifier Identifier
|
|
|
|
highlight def link idrisImport Structure
|
|
|
|
highlight def link idrisModule Structure
|
|
|
|
highlight def link idrisStructure Structure
|
|
|
|
highlight def link idrisStatement Statement
|
2020-05-19 14:40:40 -04:00
|
|
|
highlight def link idrisForall Structure
|
|
|
|
highlight def link idrisDataOpt Statement
|
2020-02-22 15:32:56 -05:00
|
|
|
highlight def link idrisDSL Statement
|
|
|
|
highlight def link idrisBlock Statement
|
|
|
|
highlight def link idrisAnnotation Statement
|
|
|
|
highlight def link idrisWhere Structure
|
|
|
|
highlight def link idrisLet Structure
|
|
|
|
highlight def link idrisTotality Statement
|
|
|
|
highlight def link idrisVisibility Statement
|
|
|
|
highlight def link idrisConditional Conditional
|
2020-05-19 14:40:40 -04:00
|
|
|
highlight def link idrisPragma Statement
|
2020-02-22 15:32:56 -05:00
|
|
|
highlight def link idrisNumber Number
|
|
|
|
highlight def link idrisFloat Float
|
|
|
|
highlight def link idrisDelimiter Delimiter
|
|
|
|
highlight def link idrisInfix PreProc
|
|
|
|
highlight def link idrisOperators Operator
|
|
|
|
highlight def link idrisType Include
|
|
|
|
highlight def link idrisDocComment Comment
|
|
|
|
highlight def link idrisLineComment Comment
|
|
|
|
highlight def link idrisBlockComment Comment
|
|
|
|
highlight def link idrisTodo Todo
|
|
|
|
highlight def link idrisMetaVar Macro
|
|
|
|
highlight def link idrisString String
|
|
|
|
highlight def link idrisChar String
|
|
|
|
highlight def link idrisBacktick Operator
|
|
|
|
|
2020-02-22 15:45:05 -05:00
|
|
|
let b:current_syntax = "idris2"
|