Changeset View
Changeset View
Standalone View
Standalone View
data/syntax/agda.xml
1 | <?xml version="1.0" encoding="UTF-8"?> | 1 | <?xml version="1.0" encoding="UTF-8"?> | ||
---|---|---|---|---|---|
2 | <!DOCTYPE language SYSTEM "language.dtd"[ | 2 | <!DOCTYPE language SYSTEM "language.dtd"[ | ||
3 | <!ENTITY charsdelim "_;."(){}@"> | 3 | <!ENTITY charsdelim "_;."(){}@"> | ||
4 | <!ENTITY wordsep "(?=([&charsdelim;]|\s|$))"> | 4 | <!ENTITY wordsep "(?=[&charsdelim;]|\s|$)"> | ||
5 | ]> | 5 | ]> | ||
6 | <language name="Agda" version="5" kateversion="5.0" section="Sources" extensions="*.agda" mimetype="text/x-agda" author="Matthias C. M. Troffaes" license="LGPL"> | 6 | <language name="Agda" version="6" kateversion="5.0" section="Sources" extensions="*.agda" mimetype="text/x-agda" author="Matthias C. M. Troffaes" license="LGPL"> | ||
7 | <highlighting> | 7 | <highlighting> | ||
8 | <list name="reserved keywords"> | 8 | <list name="reserved keywords"> | ||
9 | <item>abstract</item> | 9 | <item>abstract</item> | ||
10 | <item>codata</item> | 10 | <item>codata</item> | ||
11 | <item>coinductive</item> | 11 | <item>coinductive</item> | ||
12 | <item>constructor</item> | 12 | <item>constructor</item> | ||
13 | <item>data</item> | 13 | <item>data</item> | ||
14 | <item>do</item> | ||||
15 | <item>eta-equality</item> | ||||
14 | <item>field</item> | 16 | <item>field</item> | ||
15 | <item>forall</item> | 17 | <item>forall</item> | ||
16 | <item>hiding</item> | 18 | <item>hiding</item> | ||
17 | <item>import</item> | 19 | <item>import</item> | ||
18 | <item>in</item> | 20 | <item>in</item> | ||
19 | <item>inductive</item> | 21 | <item>inductive</item> | ||
20 | <item>infix</item> | 22 | <item>infix</item> | ||
21 | <item>infixl</item> | 23 | <item>infixl</item> | ||
22 | <item>infixr</item> | 24 | <item>infixr</item> | ||
25 | <item>instance</item> | ||||
23 | <item>let</item> | 26 | <item>let</item> | ||
27 | <item>macro</item> | ||||
28 | <item>module</item> | ||||
29 | <item>mutual</item> | ||||
30 | <item>no-eta-equality</item> | ||||
24 | <item>open</item> | 31 | <item>open</item> | ||
32 | <item>overlap</item> | ||||
25 | <item>pattern</item> | 33 | <item>pattern</item> | ||
26 | <item>postulate</item> | 34 | <item>postulate</item> | ||
27 | <item>primitive</item> | 35 | <item>primitive</item> | ||
28 | <item>private</item> | 36 | <item>private</item> | ||
29 | <item>public</item> | 37 | <item>public</item> | ||
30 | <item>module</item> | | |||
31 | <item>mutual</item> | | |||
32 | <item>quote</item> | 38 | <item>quote</item> | ||
33 | <item>quoteGoal</item> | 39 | <item>quoteGoal</item> | ||
34 | <item>quoteTerm</item> | 40 | <item>quoteTerm</item> | ||
35 | <item>record</item> | 41 | <item>record</item> | ||
36 | <item>renaming</item> | 42 | <item>renaming</item> | ||
37 | <item>rewrite</item> | 43 | <item>rewrite</item> | ||
44 | <item>tactic</item> | ||||
38 | <item>syntax</item> | 45 | <item>syntax</item> | ||
39 | <item>to</item> | 46 | <item>to</item> | ||
40 | <item>unquote</item> | 47 | <item>unquote</item> | ||
48 | <item>unquoteDecl</item> | ||||
49 | <item>unquoteDef</item> | ||||
41 | <item>using</item> | 50 | <item>using</item> | ||
51 | <item>variable</item> | ||||
42 | <item>where</item> | 52 | <item>where</item> | ||
43 | <item>with</item> | 53 | <item>with</item> | ||
44 | </list> | 54 | </list> | ||
45 | <contexts> | 55 | <contexts> | ||
46 | <context attribute="Normal" lineEndContext="#stay" name="code"> | 56 | <context attribute="Normal" lineEndContext="#stay" name="code"> | ||
47 | <RegExpr attribute="Pragma" context="#stay" String="\{-#.*#-\}" /> | 57 | <RegExpr attribute="Pragma" context="#stay" String="\{-#.*#-\}" /> | ||
48 | <keyword attribute="Keyword" context="#stay" String="reserved keywords" /> | 58 | <keyword attribute="Keyword" context="#stay" String="reserved keywords" /> | ||
49 | <RegExpr attribute="Type" context="#stay" String="(Prop|Set[₀-₉]+|Set[0-9]*)&wordsep;" /> | 59 | <RegExpr attribute="Type" context="#stay" String="(?:Prop[₀-₉]+|Prop[0-9]*|Set[₀-₉]+|Set[0-9]*)&wordsep;" /> | ||
50 | <RegExpr attribute="Special" context="#stay" String="(->|→|∀|λ|:|=|\|)&wordsep;" /> | 60 | <RegExpr attribute="Special" context="#stay" String="(?:\->|→|∀|λ|:|=|\|)&wordsep;" /> | ||
51 | <RegExpr attribute="Float" context="#stay" String="\d+\.\d+&wordsep;" /> | 61 | <RegExpr attribute="Float" context="#stay" String="\d+(?:(?:\.\d+)?[eE][+-]?\d+|\.\d+)&wordsep;" /> | ||
52 | <RegExpr attribute="Decimal" context="#stay" String="[0-9]+&wordsep;" /> | 62 | <RegExpr attribute="Decimal" context="#stay" String="[0-9]+&wordsep;" /> | ||
53 | <DetectChar attribute="Char" context="char" char="'" /> | 63 | <DetectChar attribute="Char" context="char" char="'" /> | ||
54 | <DetectChar attribute="String" context="string" char=""" /> | 64 | <DetectChar attribute="String" context="string" char=""" /> | ||
55 | <Detect2Chars attribute="Comment" context="comment" char="-" char1="-" /> | 65 | <Detect2Chars attribute="Comment" context="comment" char="-" char1="-" /> | ||
56 | <Detect2Chars attribute="Comment" context="comments" char="{" char1="-" /> | 66 | <Detect2Chars attribute="Comment" context="comments" char="{" char1="-" beginRegion="CommentBlock" /> | ||
57 | <Detect2Chars attribute="Hole" context="hole" char="{" char1="!" /> | 67 | <Detect2Chars attribute="Hole" context="hole" char="{" char1="!" /> | ||
58 | <!-- delimiters which cannot be part of an identifier, or | 68 | <!-- delimiters which cannot be part of an identifier, or | ||
59 | backslash which starts a lambda expression --> | 69 | backslash which starts a lambda expression --> | ||
60 | <AnyChar attribute="Special" context="#stay" String="&charsdelim;\\" /> | 70 | <AnyChar attribute="Special" context="#stay" String="&charsdelim;\\" /> | ||
61 | <!-- any other identifier (can contain backslash and single | 71 | <!-- any other identifier (can contain backslash and single | ||
62 | quote anywhere except at start, but these two special | 72 | quote anywhere except at start, but these two special | ||
63 | cases are already taken care off above) --> | 73 | cases are already taken care off above) --> | ||
64 | <RegExpr attribute="Normal" context="#stay" String="[^&charsdelim;\s]+" /> | 74 | <RegExpr attribute="Normal" context="#stay" String="[^&charsdelim;\s]+" /> | ||
65 | </context> | 75 | </context> | ||
66 | <context attribute="Comment" lineEndContext="#pop" name="comment" /> | 76 | <context attribute="Comment" lineEndContext="#pop" name="comment"> | ||
67 | <context attribute="Comment" lineEndContext="#stay" name="comments"> | 77 | <IncludeRules context="##Alerts" /> | ||
68 | <Detect2Chars attribute="Comment" context="comments" char="{" char1="-" /> <!-- for nested comments --> | 78 | </context> | ||
69 | <Detect2Chars attribute="Comment" context="#pop" char="-" char1="}" /> | 79 | <context attribute="Comment" lineEndContext="#stay" name="comments" noIndentationBasedFolding="1"> | ||
80 | <Detect2Chars attribute="Comment" context="comments" char="{" char1="-" beginRegion="CommentBlock" /> <!-- for nested comments --> | ||||
81 | <Detect2Chars attribute="Comment" context="#pop" char="-" char1="}" endRegion="CommentBlock" /> | ||||
82 | <IncludeRules context="##Alerts" /> | ||||
70 | </context> | 83 | </context> | ||
71 | <context attribute="Hole" lineEndContext="#stay" name="hole"> | 84 | <context attribute="Hole" lineEndContext="#stay" name="hole"> | ||
72 | <Detect2Chars attribute="Hole" context="#pop" char="!" char1="}" /> | 85 | <Detect2Chars attribute="Hole" context="#pop" char="!" char1="}" /> | ||
73 | </context> | 86 | </context> | ||
74 | <context attribute="Char" lineEndContext="#pop" name="char"> | 87 | <context attribute="Char" lineEndContext="#pop" name="char"> | ||
75 | <Detect2Chars attribute="Char" context="#stay" char="\" char1="'" /> | 88 | <Detect2Chars attribute="Char" context="#stay" char="\" char1="'" /> | ||
76 | <DetectChar attribute="Char" context="#pop" char="'" /> | 89 | <DetectChar attribute="Char" context="#pop" char="'" /> | ||
77 | </context> | 90 | </context> | ||
Show All 15 Lines | 96 | <itemDatas> | |||
93 | <itemData name="Char" defStyleNum="dsChar" spellChecking="false" /> | 106 | <itemData name="Char" defStyleNum="dsChar" spellChecking="false" /> | ||
94 | <itemData name="String" defStyleNum="dsString" /> | 107 | <itemData name="String" defStyleNum="dsString" /> | ||
95 | </itemDatas> | 108 | </itemDatas> | ||
96 | </highlighting> | 109 | </highlighting> | ||
97 | <general> | 110 | <general> | ||
98 | <folding indentationsensitive="1"/> | 111 | <folding indentationsensitive="1"/> | ||
99 | <comments> | 112 | <comments> | ||
100 | <comment name="singleLine" start="--" /> | 113 | <comment name="singleLine" start="--" /> | ||
101 | <comment name="multiLine" start="{-" end="-}" /> | 114 | <comment name="multiLine" start="{-" end="-}" region="CommentBlock" /> | ||
102 | </comments> | 115 | </comments> | ||
103 | <keywords casesensitive="1" | 116 | <keywords casesensitive="1" | ||
104 | weakDeliminator=":!+,-<=>%&*/?[]^|~\\" | 117 | weakDeliminator=":!+,-<=>%&*/?[]^|~\\" | ||
105 | additionalDeliminator="&charsdelim;" /> | 118 | additionalDeliminator="&charsdelim;" /> | ||
106 | </general> | 119 | </general> | ||
107 | </language> | 120 | </language> |