@@ -4,7 +4,7 @@
4" highlighter to support idris.
4" highlighter to support idris.
6" author: raichoo (raichoo@googlemail.com)
6" author: raichoo (raichoo@googlemail.com)
7−" date: Feb 25 2013
7+" date: Mar 11 2013
9syn match idrisModule "\<\(module\|namespace\)\>"
9syn match idrisModule "\<\(module\|namespace\)\>"
10syn match idrisImport "\<import\>"
10syn match idrisImport "\<import\>"
@@ -15,7 +15,7 @@ syn match idrisAnnotation "\<\(total\|partial\|auto\|impossible\|static\|implici
15syn match idrisStatement "\<\(do\|case\|of\|let\|in\|with\)\>"
15syn match idrisStatement "\<\(do\|case\|of\|let\|in\|with\)\>"
16syn match idrisSyntax "\(pattern \+\|term \+\)\?syntax"
16syn match idrisSyntax "\(pattern \+\|term \+\)\?syntax"
17syn match idrisConditional "\<\(if\|then\|else\)\>"
17syn match idrisConditional "\<\(if\|then\|else\)\>"
18−syn match idrisTactic contained "\<\(intros\?\|rewrite\|exact\|refine\|trivial\|let\|focus\|try\|compute\|solve\|attack\)\>"
18+syn match idrisTactic contained "\<\(intros\?\|rewrite\|exact\|refine\|trivial\|let\|focus\|try\|compute\|solve\|attack\|reflect\)\>"
19syn match idrisNumber "\<[0-9]\+\>\|\<0[xX][0-9a-fA-F]\+\>\|\<0[oO][0-7]\+\>"
19syn match idrisNumber "\<[0-9]\+\>\|\<0[xX][0-9a-fA-F]\+\>\|\<0[oO][0-7]\+\>"
20syn match idrisFloat "\<[0-9]\+\.[0-9]\+\([eE][-+]\=[0-9]\+\)\=\>"
20syn match idrisFloat "\<[0-9]\+\.[0-9]\+\([eE][-+]\=[0-9]\+\)\=\>"
21syn match idrisDelimiter "(\|)\|\[\|\]\|,\|;\|_\|{\|}"
21syn match idrisDelimiter "(\|)\|\[\|\]\|,\|;\|_\|{\|}"
@@ -28,7 +28,7 @@ syn match idrisLink "%\(lib\|link\|include\)"
28syn match idrisDirective "%\(access\|default\|assert_total\)"
28syn match idrisDirective "%\(access\|default\|assert_total\)"
29syn region idrisString start=+"+ skip=+\\\\\|\\"+ end=+"+
29syn region idrisString start=+"+ skip=+\\\\\|\\"+ end=+"+
30syn region idrisBlockComment start="{-" end="-}"
30syn region idrisBlockComment start="{-" end="-}"
31−syn region idrisProofBlock start="\(default\s\+\)\?proof *{" end="}" contains=idrisTactic
31+syn region idrisProofBlock start="\(default\s\+\)\?\(proof\|tactics\) *{" end="}" contains=idrisTactic
33syn match idrisBadLeadingWhiteSpace "^\s*\t\+"
33syn match idrisBadLeadingWhiteSpace "^\s*\t\+"
34syn match idrisBadTrailingWhiteSpace "\s\+$"
34syn match idrisBadTrailingWhiteSpace "\s\+$"