ale_linters/dafny/dafny.vim

   1 " Author: Taylor Blau <me@ttaylorr.com>
   2 call ale#Set('dafny_dafny_timelimit', 10)
   3
   4 function! ale_linters#dafny#dafny#Handle(buffer, lines) abort
   5     let l:pattern = '\v(.*)\((\d+),(\d+)\): (.*): (.*)'
   6     let l:output = []
   7
   8     for l:match in ale#util#GetMatches(a:lines, l:pattern)
   9         call add(l:output, {
  10         \    'filename': l:match[1],
  11         \    'col': l:match[3] + 0,
  12         \    'lnum': l:match[2] + 0,
  13         \    'text': l:match[5],
  14         \    'type': l:match[4] =~# '^Error' ? 'E' : 'W'
  15         \ })
  16     endfor
  17
  18     for l:match in ale#util#GetMatches(a:lines, '\v(.*)\((\d+),(\d+)\): (Verification of .{-} timed out after \d+ seconds)')
  19         call add(l:output, {
  20         \     'filename': l:match[1],
  21         \     'col': l:match[3] + 0,
  22         \     'lnum': l:match[2] + 0,
  23         \     'text': l:match[4],
  24         \     'type': 'E',
  25         \ })
  26     endfor
  27
  28     return l:output
  29 endfunction
  30
  31 function! ale_linters#dafny#dafny#GetCommand(buffer) abort
  32     return printf('dafny %%s /compile:0 /timeLimit:%d', ale#Var(a:buffer, 'dafny_dafny_timelimit'))
  33 endfunction
  34
  35 call ale#linter#Define('dafny', {
  36 \    'name': 'dafny',
  37 \    'executable': 'dafny',
  38 \    'command': function('ale_linters#dafny#dafny#GetCommand'),
  39 \    'callback': 'ale_linters#dafny#dafny#Handle',
  40 \    'lint_file': 1,
  41 \ })