git.iko.soy/Idris-dev
on master help sign in
Merge branch 'master' of github.com:edwinb/Idris-dev
commit9f1141e9dda705530517ac0b18e89aae29c00361 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 20 Mar 2013, 12:15 (14 years ago) parent9724992d48b5ef
6 files changed+225−3
compare with master
unifiedsplit
contribs/tool-support/sublime-text/Idris/Idris.JSON-tmLanguage+70 contribs/tool-support/sublime-text/Idris/Idris.tmLanguage+126 contribs/tool-support/sublime-text/Idris/idris.sublime-build+5 contribs/tool-support/sublime-text/README.md+11 contribs/tool-support/vim/indent/idris.vim+11−1 contribs/tool-support/vim/syntax/idris.vim+2−2
contribs/tool-support/sublime-text/Idris/Idris.JSON-tmLanguagenew file+70
@@ -0,0 +1,70 @@
1+{ "name": "Idris",
2+ "scopeName": "source.idris",
3+ "fileTypes": ["idr"],
4+ "patterns": [
5+ { "name": "keyword.control.idris",
6+ "match": "\\b(if|then|else|do|let|in|data|codata|record|dsl|import)\\b"
7+
8+ },
9+ { "name": "keyword.control.idris",
10+ "match": "\\b(impossible|case|of|total|partial|mutual|infix|infixl|infixr)\\b"
11+
12+ },
13+ { "name": "keyword.control.idris",
14+ "match": "\\b(where|with|syntax|proof|postulate|using|namespace|class|instance)\\b"
15+
16+ },
17+ { "name": "keyword.control.idris",
18+ "match": "\\b(public|private|abstract|implicit)\\b"
19+
20+ },
21+ { "name": "keyword.other.idris",
22+ "match": "\\b(Type|Int|Integer|Float|Char|String|Ptr|Bits8|Bits16|Bits32|Bits64)\\b"
23+ },
24+ { "name": "constant.numeric.idris",
25+ "match": "\\b(S|O)\\b"
26+ },
27+ { "match": "\\b([0-9]+|0([xX][0-9a-fA-F]+|[oO][0-7]+))\\b",
28+ "name": "constant.numeric.idris",
29+ "comment": "integers"
30+ },
31+ {
32+ "match": "\\b([0-9]+\\.[0-9]+([eE][+-]?[0-9]+)?|[0-9]+[eE][+-]?[0-9]+)\\b",
33+ "name": "constant.numeric.float.idris",
34+ "comment": "floats"
35+ },
36+ {
37+ "name": "comment.line.idris",
38+ "match": "(--).*$\n?",
39+ "comment": "Line comment"
40+ },
41+ { "name": "comment.block.idris",
42+ "begin": "\\{-",
43+ "end": "-\\}",
44+ "comment": "Block comment"
45+ },
46+ {
47+ "name": "string.quoted.idris",
48+ "begin": "\"",
49+ "beginCaptures": {
50+ "0": { "name": "punctuation.definition.string.begin.idris"}
51+ },
52+ "end": "\"",
53+ "endCaptures": {
54+ "0": { "name": "punctuation.definition.string.end.idris"}
55+ },
56+ "patterns": [
57+ { "name": "constant.character.escape.idris",
58+ "match": "\\\\\""
59+ }
60+ ]
61+
62+ }
63+
64+
65+ ],
66+ "repository": {
67+
68+ },
69+ "uuid": "4dd16092-ffa5-4ba4-8075-e5da9f368a72"
70+}
contribs/tool-support/sublime-text/Idris/Idris.tmLanguagenew file+126
@@ -0,0 +1,126 @@
1+<?xml version="1.0" encoding="UTF-8"?>
2+<!DOCTYPE plist PUBLIC "-//Apple Computer//DTD PLIST 1.0//EN" "http://www.apple.com/DTDs/PropertyList-1.0.dtd">
3+<plist version="1.0">
4+<dict>
5+ <key>fileTypes</key>
6+ <array>
7+ <string>idr</string>
8+ </array>
9+ <key>name</key>
10+ <string>Idris</string>
11+ <key>patterns</key>
12+ <array>
13+ <dict>
14+ <key>match</key>
15+ <string>\b(if|then|else|do|let|in|data|codata|record|dsl|import)\b</string>
16+ <key>name</key>
17+ <string>keyword.control.idris</string>
18+ </dict>
19+ <dict>
20+ <key>match</key>
21+ <string>\b(impossible|case|of|total|partial|mutual|infix|infixl|infixr)\b</string>
22+ <key>name</key>
23+ <string>keyword.control.idris</string>
24+ </dict>
25+ <dict>
26+ <key>match</key>
27+ <string>\b(where|with|syntax|proof|postulate|using|namespace|class|instance)\b</string>
28+ <key>name</key>
29+ <string>keyword.control.idris</string>
30+ </dict>
31+ <dict>
32+ <key>match</key>
33+ <string>\b(public|private|abstract|implicit)\b</string>
34+ <key>name</key>
35+ <string>keyword.control.idris</string>
36+ </dict>
37+ <dict>
38+ <key>match</key>
39+ <string>\b(Type|Int|Integer|Float|Char|String|Ptr|Bits8|Bits16|Bits32|Bits64)\b</string>
40+ <key>name</key>
41+ <string>keyword.other.idris</string>
42+ </dict>
43+ <dict>
44+ <key>match</key>
45+ <string>\b(S|O)\b</string>
46+ <key>name</key>
47+ <string>constant.numeric.idris</string>
48+ </dict>
49+ <dict>
50+ <key>comment</key>
51+ <string>integers</string>
52+ <key>match</key>
53+ <string>\b([0-9]+|0([xX][0-9a-fA-F]+|[oO][0-7]+))\b</string>
54+ <key>name</key>
55+ <string>constant.numeric.idris</string>
56+ </dict>
57+ <dict>
58+ <key>comment</key>
59+ <string>floats</string>
60+ <key>match</key>
61+ <string>\b([0-9]+\.[0-9]+([eE][+-]?[0-9]+)?|[0-9]+[eE][+-]?[0-9]+)\b</string>
62+ <key>name</key>
63+ <string>constant.numeric.float.idris</string>
64+ </dict>
65+ <dict>
66+ <key>comment</key>
67+ <string>Line comment</string>
68+ <key>match</key>
69+ <string>(--).*$
70+?</string>
71+ <key>name</key>
72+ <string>comment.line.idris</string>
73+ </dict>
74+ <dict>
75+ <key>begin</key>
76+ <string>\{-</string>
77+ <key>comment</key>
78+ <string>Block comment</string>
79+ <key>end</key>
80+ <string>-\}</string>
81+ <key>name</key>
82+ <string>comment.block.idris</string>
83+ </dict>
84+ <dict>
85+ <key>begin</key>
86+ <string>"</string>
87+ <key>beginCaptures</key>
88+ <dict>
89+ <key>0</key>
90+ <dict>
91+ <key>name</key>
92+ <string>punctuation.definition.string.begin.idris</string>
93+ </dict>
94+ </dict>
95+ <key>end</key>
96+ <string>"</string>
97+ <key>endCaptures</key>
98+ <dict>
99+ <key>0</key>
100+ <dict>
101+ <key>name</key>
102+ <string>punctuation.definition.string.end.idris</string>
103+ </dict>
104+ </dict>
105+ <key>name</key>
106+ <string>string.quoted.idris</string>
107+ <key>patterns</key>
108+ <array>
109+ <dict>
110+ <key>match</key>
111+ <string>\\"</string>
112+ <key>name</key>
113+ <string>constant.character.escape.idris</string>
114+ </dict>
115+ </array>
116+ </dict>
117+ </array>
118+ <key>repository</key>
119+ <dict>
120+ </dict>
121+ <key>scopeName</key>
122+ <string>source.idris</string>
123+ <key>uuid</key>
124+ <string>4dd16092-ffa5-4ba4-8075-e5da9f368a72</string>
125+</dict>
126+</plist>
contribs/tool-support/sublime-text/Idris/idris.sublime-buildnew file+5
@@ -0,0 +1,5 @@
1+{
2+ "cmd": ["idris", "$file"],
3+ "file_regex": "^(...*?):([0-9]*):?([0-9]*)",
4+ "selector": "source.idris"
5+}
contribs/tool-support/sublime-text/README.mdnew file+11
@@ -0,0 +1,11 @@
1+#### Idris support for Sublime Text 2
2+
3+To install, copy the Idris directory to Sublime Text's Packages directory.
4+
5+To build a new Idris.tmLanguage file from the Idris.JSON-tmLanguage file, Sublime Text needs to have the AAAPackageDev package installed.
6+
7+Syntax Definitions tutorial: https://sublime-text-unofficial-documentation.readthedocs.org/en/latest/extensibility/syntaxdefs.html
8+
9+Syntax Definitions reference: https://sublime-text-unofficial-documentation.readthedocs.org/en/latest/reference/syntaxdefs.html
10+
11+Most used scopes: http://manual.macromates.com/en/language_grammars#naming_conventions
contribs/tool-support/vim/indent/idris.vim+11−1
@@ -3,7 +3,7 @@
33" Based on haskell indentation by motemen <motemen@gmail.com>
44"
55" author: raichoo (raichoo@googlemail.com)
6−" date: Nov 2 2012
6+" date: Mar 19 2013
77"
88" Modify g:idris_indent_if and g:idris_indent_case to
99" change indentation for `if'(default 3) and `case'(default 5).
@@ -36,6 +36,12 @@ if !exists('g:idris_indent_let')
3636 let g:idris_indent_let = 4
3737endif
3838
39+if !exists('g:idris_indent_rewrite')
40+ " rewrite prf in expr
41+ " >>>>x
42+ let g:idris_indent_rewrite = 8
43+endif
44+
3945if !exists('g:idris_indent_where')
4046 " where f : Nat -> Nat
4147 " >>>>>>f x = x
@@ -71,6 +77,10 @@ function! GetIdrisIndent()
7177 return match(prevline, 'let') + g:idris_indent_let
7278 endif
7379
80+ if prevline =~ '\<rewrite\>\s\+.\+\<in\>\s*$'
81+ return match(prevline, 'rewrite') + g:idris_indent_rewrite
82+ endif
83+
7484 if prevline !~ '\<else\>'
7585 let s = match(prevline, '\<if\>.*\&.*\zs\<then\>')
7686 if s > 0
contribs/tool-support/vim/syntax/idris.vim+2−2
@@ -4,7 +4,7 @@
44" highlighter to support idris.
55"
66" author: raichoo (raichoo@googlemail.com)
7−" date: Mar 12 2013
7+" date: Mar 19 2013
88
99syn match idrisModule "\<\(module\|namespace\)\>"
1010syn match idrisImport "\<import\>"
@@ -12,7 +12,7 @@ syn match idrisStructure "\<\(class\|\(co\)\?data\|instance\|where\|record\|dsl\
1212syn match idrisVisibility "\<\(public\|abstract\|private\)\>"
1313syn match idrisBlock "\<\(parameters\|mutual\|postulate\|using\)\>"
1414syn match idrisAnnotation "\<\(total\|partial\|auto\|impossible\|static\|implicit\)\>"
15−syn match idrisStatement "\<\(do\|case\|of\|let\|in\|with\)\>"
15+syn match idrisStatement "\<\(do\|case\|of\|rewrite\|let\|in\|with\)\>"
1616syn match idrisSyntax "\(pattern \+\|term \+\)\?syntax"
1717syn match idrisConditional "\<\(if\|then\|else\)\>"
1818syn match idrisTactic contained "\<\(intros\?\|rewrite\|exact\|refine\|trivial\|let\|focus\|try\|compute\|solve\|attack\|reflect\)\>"