diff options
| -rw-r--r-- | README.md | 1 | ||||
| -rw-r--r-- | ale_linters/dafny/dafny.vim | 24 | ||||
| -rw-r--r-- | doc/ale.txt | 1 | ||||
| -rw-r--r-- | test/handler/test_dafny_handler.vader | 26 |
4 files changed, 52 insertions, 0 deletions
@@ -87,6 +87,7 @@ formatting. | CSS | [csslint](http://csslint.net/), [stylelint](https://github.com/stylelint/stylelint), [prettier](https://github.com/prettier/prettier) | | Cython (pyrex filetype) | [cython](http://cython.org/) | | D | [dmd](https://dlang.org/dmd-linux.html) | +| Dafny | [dafny](https://rise4fun.com/Dafny) | | Dart | [dartanalyzer](https://github.com/dart-lang/sdk/tree/master/pkg/analyzer_cli) !!, [language_server](https://github.com/natebosch/dart_language_server) | | Dockerfile | [hadolint](https://github.com/lukasmartinelli/hadolint) | | Elixir | [credo](https://github.com/rrrene/credo), [dogma](https://github.com/lpil/dogma) !! | diff --git a/ale_linters/dafny/dafny.vim b/ale_linters/dafny/dafny.vim new file mode 100644 index 00000000..8f6c62bc --- /dev/null +++ b/ale_linters/dafny/dafny.vim @@ -0,0 +1,24 @@ +" Author: Taylor Blau <me@ttaylorr.com> + +function! ale_linters#dafny#dafny#Handle(buffer, lines) abort + let l:pattern = '\v(.*)\((\d+),(\d+)\): (.*): (.*)' + let l:output = [] + + for l:match in ale#util#GetMatches(a:lines, l:pattern) + call add(l:output, { + \ 'bufnr': a:buffer, + \ 'col': l:match[3] + 0, + \ 'lnum': l:match[2] + 0, + \ 'text': l:match[5], + \ 'type': l:match[4] =~# '^Error' ? 'E' : 'W' + \ }) + endfor + return l:output +endfunction + +call ale#linter#Define('dafny', { +\ 'name': 'dafny', +\ 'executable': 'dafny', +\ 'command': 'dafny %s /compile:0', +\ 'callback': 'ale_linters#dafny#dafny#Handle', +\ }) diff --git a/doc/ale.txt b/doc/ale.txt index d3efcc13..9ca0c727 100644 --- a/doc/ale.txt +++ b/doc/ale.txt @@ -270,6 +270,7 @@ Notes: * CSS: `csslint`, `stylelint`, `prettier` * Cython (pyrex filetype): `cython` * D: `dmd` +* Dafny: `dafny`!! * Dart: `dartanalyzer`!!, `language_server` * Dockerfile: `hadolint` * Elixir: `credo`, `dogma`!! diff --git a/test/handler/test_dafny_handler.vader b/test/handler/test_dafny_handler.vader new file mode 100644 index 00000000..1de9a77f --- /dev/null +++ b/test/handler/test_dafny_handler.vader @@ -0,0 +1,26 @@ +Execute(The Dafny handler should parse output correctly): + runtime ale_linters/dafny/dafny.vim + AssertEqual + \ [ + \ { + \ 'bufnr': 0, + \ 'col': 45, + \ 'lnum': 123, + \ 'text': 'A precondition for this call might not hold.', + \ 'type': 'E' + \ }, + \ { + \ 'bufnr': 0, + \ 'col': 90, + \ 'lnum': 678, + \ 'text': 'This is the precondition that might not hold.', + \ 'type': 'W' + \ } + \ ], + \ ale_linters#dafny#dafny#Handle(0, [ + \ 'File.dfy(123,45): Error BP5002: A precondition for this call might not hold.', + \ 'File.dfy(678,90): Related location: This is the precondition that might not hold.' + \ ]) + +After: + call ale#linter#Reset() |