if exists('g:polyglot_disabled') && index(g:polyglot_disabled, 'idris') != -1 finish endif " indentation for idris (idris-lang.org) " " Based on haskell indentation by motemen " " author: raichoo (raichoo@googlemail.com) " " Modify g:idris_indent_if and g:idris_indent_case to " change indentation for `if'(default 3) and `case'(default 5). " Example (in .vimrc): " > let g:idris_indent_if = 2 if exists('b:did_indent') finish endif let b:did_indent = 1 if !exists('g:idris_indent_if') " if bool " >>>then ... " >>>else ... let g:idris_indent_if = 3 endif if !exists('g:idris_indent_case') " case xs of " >>>>>[] => ... " >>>>>(y::ys) => ... let g:idris_indent_case = 5 endif if !exists('g:idris_indent_let') " let x : Nat = O in " >>>>x let g:idris_indent_let = 4 endif if !exists('g:idris_indent_rewrite') " rewrite prf in expr " >>>>>>>>x let g:idris_indent_rewrite = 8 endif if !exists('g:idris_indent_where') " where f : Nat -> Nat " >>>>>>f x = x let g:idris_indent_where = 6 endif if !exists('g:idris_indent_do') " do x <- a " >>>y <- b let g:idris_indent_do = 3 endif setlocal indentexpr=GetIdrisIndent() setlocal indentkeys=!^F,o,O,} function! GetIdrisIndent() let prevline = getline(v:lnum - 1) if prevline =~ '\s\+(\s*.\+\s\+:\s\+.\+\s*)\s\+->\s*$' return match(prevline, '(') elseif prevline =~ '\s\+{\s*.\+\s\+:\s\+.\+\s*}\s\+->\s*$' return match(prevline, '{') endif if prevline =~ '[!#$%&*+./<>?@\\^|~-]\s*$' let s = match(prevline, '[:=]') if s > 0 return s + 2 else return match(prevline, '\S') endif endif if prevline =~ '[{([][^})\]]\+$' return match(prevline, '[{([]') endif if prevline =~ '\\s\+.\+\\s*$' return match(prevline, '\') + g:idris_indent_let endif if prevline =~ '\\s\+.\+\\s*$' return match(prevline, '\') + g:idris_indent_rewrite endif if prevline !~ '\' let s = match(prevline, '\.*\&.*\zs\') if s > 0 return s endif let s = match(prevline, '\') if s > 0 return s + g:idris_indent_if endif endif if prevline =~ '\(\\|\\|=\|[{([]\)\s*$' return match(prevline, '\S') + &shiftwidth endif if prevline =~ '\\s\+\S\+.*$' return match(prevline, '\') + g:idris_indent_where endif if prevline =~ '\\s\+\S\+.*$' return match(prevline, '\') + g:idris_indent_do endif if prevline =~ '^\s*\<\(co\)\?data\>\s\+[^=]\+\s\+=\s\+\S\+.*$' return match(prevline, '=') endif if prevline =~ '\\s\+([^)]*)\s*$' return match(prevline, '\S') + &shiftwidth endif if prevline =~ '\\s\+.\+\\s*$' return match(prevline, '\') + g:idris_indent_case endif if prevline =~ '^\s*\(\\|\<\(co\)\?data\>\)\s\+\S\+\s*$' return match(prevline, '\(\\|\<\(co\)\?data\>\)') + &shiftwidth endif if prevline =~ '^\s*\(\\|\\)\s*([^(]*)\s*$' return match(prevline, '\(\\|\\)') + &shiftwidth endif if prevline =~ '^\s*\\s*$' return match(prevline, '\') + &shiftwidth endif let line = getline(v:lnum) if (line =~ '^\s*}\s*' && prevline !~ '^\s*;') return match(prevline, '\S') - &shiftwidth endif return match(prevline, '\S') endfunction