git.iko.soy/Idris-dev
on master help sign in
Merge pull request #67 from raichoo/master
4863bebEdwin Brady
contribs/tool-support/vim/indent/idris.vim+14−4
compare with master
unifiedsplit
@@ -3,7 +3,7 @@
3" Based on haskell indentation by motemen <motemen@gmail.com>
3" Based on haskell indentation by motemen <motemen@gmail.com>
4"
4"
5" author: raichoo (raichoo@googlemail.com)
5" author: raichoo (raichoo@googlemail.com)
6−" date: Oct 19 2012
6+" date: Oct 31 2012
7"
7"
8" Modify g:idris_indent_if and g:idris_indent_case to
8" Modify g:idris_indent_if and g:idris_indent_case to
9" change indentation for `if'(default 3) and `case'(default 5).
9" change indentation for `if'(default 3) and `case'(default 5).
@@ -49,7 +49,7 @@ if !exists('g:idris_indent_do')
49endif
49endif
50
50
51setlocal indentexpr=GetIdrisIndent()
51setlocal indentexpr=GetIdrisIndent()
52−setlocal indentkeys=!^F,o,O
52+setlocal indentkeys=!^F,o,O,}
53
53
54function! GetIdrisIndent()
54function! GetIdrisIndent()
55 let prevline = getline(v:lnum - 1)
55 let prevline = getline(v:lnum - 1)
@@ -63,7 +63,7 @@ function! GetIdrisIndent()
63 endif
63 endif
64 endif
64 endif
65
65
66− if prevline =~ '[{([]\s*$'
66+ if prevline =~ '[{([][^})\]]\+$'
67 return match(prevline, '[{([]')
67 return match(prevline, '[{([]')
68 endif
68 endif
69
69
@@ -83,7 +83,7 @@ function! GetIdrisIndent()
83 endif
83 endif
84 endif
84 endif
85
85
86− if prevline =~ '\(where\|do\|=\)\s*$'
86+ if prevline =~ '\(where\|do\|=\|[{([]\)\s*$'
87 return match(prevline, '\S') + &shiftwidth
87 return match(prevline, '\S') + &shiftwidth
88 endif
88 endif
89
89
@@ -115,5 +115,15 @@ function! GetIdrisIndent()
115 return match(prevline, '\(using\|parameters\)') + &shiftwidth
115 return match(prevline, '\(using\|parameters\)') + &shiftwidth
116 endif
116 endif
117
117
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+
118 return match(prevline, '\S')
128 return match(prevline, '\S')
119endfunction
129endfunction
contribs/tool-support/vim/syntax/idris.vim+2−2
@@ -4,13 +4,13 @@
4" highlighter to support idris.
4" highlighter to support idris.
5"
5"
6" author: raichoo (raichoo@googlemail.com)
6" author: raichoo (raichoo@googlemail.com)
7−" date: Sep 21 2012
7+" date: Oct 31 2012
8
8
9syn match idrisModule "\<\(module\|namespace\)\>"
9syn match idrisModule "\<\(module\|namespace\)\>"
10syn match idrisImport "\<import\>"
10syn match idrisImport "\<import\>"
11syn match idrisStructure "\<\(class\|\(co\)\?data\|instance\|where\|record\)\>"
11syn match idrisStructure "\<\(class\|\(co\)\?data\|instance\|where\|record\)\>"
12syn match idrisVisibility "\<\(public\|abstract\|private\)\>"
12syn 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\)\>"
14syn match idrisSyntax "\(pattern \+\|term \+\)\?syntax"
14syn match idrisSyntax "\(pattern \+\|term \+\)\?syntax"
15syn match idrisConditional "\<\(if\|then\|else\)\>"
15syn match idrisConditional "\<\(if\|then\|else\)\>"
16syn match idrisTactic contained "\<\(intros\?\|rewrite\|exact\|refine\|trivial\|let\|focus\|try\|compute\|solve\|attack\)\>"
16syn 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 =
32showProof :: Bool -> Name -> [String] -> String
32showProof :: Bool -> Name -> [String] -> String
33showProof lit n ps
33showProof lit n ps
34 = bird ++ show n ++ " = proof {" ++ break ++
34 = bird ++ show n ++ " = proof {" ++ break ++
35− showSep break (map (\x -> " " ++ x ++ ";") ps) ++
35+ showSep break (map (\x -> " " ++ x ++ ";") ps) ++
36 break ++ "}\n"
36 break ++ "}\n"
37 where bird = if lit then "> " else ""
37 where bird = if lit then "> " else ""
38 break = "\n" ++ bird
38 break = "\n" ++ bird