git.iko.soy/Idris-dev
on master help sign in
Merge pull request #67 from raichoo/master

vim support for new features and indent adjustment for proof adding

commit4863bebee67b78ae4381cd5c265c6502287539a9 authorEdwin Brady <edwin.brady@gmail.com> dateWed 31 Oct 2012, 14:18 (14 years ago) parent29c67e9c3446b2
3 files changed+17−7
compare with master
unifiedsplit
contribs/tool-support/vim/indent/idris.vim+14−4 contribs/tool-support/vim/syntax/idris.vim+2−2 src/Idris/Prover.hs+1−1
contribs/tool-support/vim/indent/idris.vim+14−4
@@ -3,7 +3,7 @@
33" Based on haskell indentation by motemen <motemen@gmail.com>
44"
55" author: raichoo (raichoo@googlemail.com)
6−" date: Oct 19 2012
6+" date: Oct 31 2012
77"
88" Modify g:idris_indent_if and g:idris_indent_case to
99" change indentation for `if'(default 3) and `case'(default 5).
@@ -49,7 +49,7 @@ if !exists('g:idris_indent_do')
4949endif
5050
5151setlocal indentexpr=GetIdrisIndent()
52−setlocal indentkeys=!^F,o,O
52+setlocal indentkeys=!^F,o,O,}
5353
5454function! GetIdrisIndent()
5555 let prevline = getline(v:lnum - 1)
@@ -63,7 +63,7 @@ function! GetIdrisIndent()
6363 endif
6464 endif
6565
66− if prevline =~ '[{([]\s*$'
66+ if prevline =~ '[{([][^})\]]\+$'
6767 return match(prevline, '[{([]')
6868 endif
6969
@@ -83,7 +83,7 @@ function! GetIdrisIndent()
8383 endif
8484 endif
8585
86− if prevline =~ '\(where\|do\|=\)\s*$'
86+ if prevline =~ '\(where\|do\|=\|[{([]\)\s*$'
8787 return match(prevline, '\S') + &shiftwidth
8888 endif
8989
@@ -115,5 +115,15 @@ function! GetIdrisIndent()
115115 return match(prevline, '\(using\|parameters\)') + &shiftwidth
116116 endif
117117
118+ if prevline =~ '^\s*mutual\s*$'
119+ return match(prevline, 'mutual') + &shiftwidth
120+ endif
121+
122+ let line = getline(v:lnum)
123+
124+ if (line =~ '^\s*}\s*' && prevline !~ '^\s*;')
125+ return match(prevline, '\S') - &shiftwidth
126+ endif
127+
118128 return match(prevline, '\S')
119129endfunction
contribs/tool-support/vim/syntax/idris.vim+2−2
@@ -4,13 +4,13 @@
44" highlighter to support idris.
55"
66" author: raichoo (raichoo@googlemail.com)
7−" date: Sep 21 2012
7+" date: Oct 31 2012
88
99syn match idrisModule "\<\(module\|namespace\)\>"
1010syn match idrisImport "\<import\>"
1111syn match idrisStructure "\<\(class\|\(co\)\?data\|instance\|where\|record\)\>"
1212syn match idrisVisibility "\<\(public\|abstract\|private\)\>"
13−syn match idrisStatement "\<\(do\|case\|of\|let\|in\|with\|total\|dsl\|auto\|using\|parameters\)\>"
13+syn match idrisStatement "\<\(do\|case\|of\|let\|in\|with\|total\|dsl\|auto\|using\|parameters\|mutual\)\>"
1414syn match idrisSyntax "\(pattern \+\|term \+\)\?syntax"
1515syn match idrisConditional "\<\(if\|then\|else\)\>"
1616syn match idrisTactic contained "\<\(intros\?\|rewrite\|exact\|refine\|trivial\|let\|focus\|try\|compute\|solve\|attack\)\>"
src/Idris/Prover.hs+1−1
@@ -32,7 +32,7 @@ prover lit x =
3232showProof :: Bool -> Name -> [String] -> String
3333showProof lit n ps
3434 = bird ++ show n ++ " = proof {" ++ break ++
35− showSep break (map (\x -> " " ++ x ++ ";") ps) ++
35+ showSep break (map (\x -> " " ++ x ++ ";") ps) ++
3636 break ++ "}\n"
3737 where bird = if lit then "> " else ""
3838 break = "\n" ++ bird