<styles>
<style id="comment" _name="Comment" map-to="def:comment"/>
- <style id="base-n-integer" _name="Base-N Integer" map-to="def:base-n-integer"/>
<style id="string" _name="String" map-to="def:string"/>
+ <style id="escape" _name="Escape" map-to="def:string"/>
<style id="keyword" _name="Keyword" map-to="def:keyword"/>
<style id="type" _name="Data Type" map-to="def:type"/>
- <style id="escape" _name="Escaped Character" map-to="def:special-char"/>
+ <style id="latex" _name="LaTeX Escaped" map-to="def:special-char"/>
+ <style id="macros" _name="Macros" map-to="def:keyword"/>
+ <style id="tinycals" _name="Tinycals" map-to="def:keyword"/>
+ <style id="quantifiers" _name="Quantifiers" map-to="def:type"/>
</styles>
<definitions>
- <define-regex id="cap-ident">\b[A-Z][A-Za-z0-9_']*</define-regex>
- <define-regex id="low-ident">\b[a-z][A-Za-z0-9_']*</define-regex>
- <define-regex id="char-esc">\\((\\|"|'|n|t|b|r)|[0-9]{3}|x[0-9a-fA-F]{2})</define-regex>
+ <define-regex id="char-esc">\\"|[0-9a-zA-Z]</define-regex>
<context id="escape-seq" style-ref="escape">
<match>\%{char-esc}</match>
</context>
<context id="character-constant" style-ref="string">
<match>('\%{char-esc}')|('[^\\']')</match>
</context>
+ <context id="whelp_macros" style-ref="macros">
+ <prefix>whelp *</prefix>
+ <keyword>elim</keyword>
+ <keyword>hint</keyword>
+ <keyword>instance</keyword>
+ <keyword>locate</keyword>
+ <keyword>match</keyword>
+ </context>
+ <context id="latex" style-ref="latex">
+ <prefix>\\</prefix>
+ <keyword>def</keyword>
+ <keyword>forall</keyword>
+ <keyword>lambda</keyword>
+ <keyword>to</keyword>
+ <keyword>exists</keyword>
+ <keyword>Rightarrow</keyword>
+ <keyword>Assign</keyword>
+ <keyword>land</keyword>
+ <keyword>lor</keyword>
+ <keyword>lnot</keyword>
+ <keyword>liff</keyword>
+ <keyword>subst</keyword>
+ <keyword>vdash</keyword>
+ <keyword>iforall</keyword>
+ <keyword>iexists</keyword>
+ </context>
<!-- Flow control & common keywords -->
<context id="keywords" style-ref="keyword">
<!-- objects -->
<keyword>ncoinductive</keyword>
<keyword>nlet</keyword>
<keyword>nlemma</keyword>
+ <keyword>nremark</keyword>
<keyword>naxiom</keyword>
<!-- tactics -->
<!-- ntactics -->
<keyword>napply</keyword>
+ <keyword>napplyS</keyword>
<keyword>ncases</keyword>
<keyword>nletin</keyword>
<keyword>nauto</keyword>
<keyword>nchange</keyword>
<keyword>nrewrite</keyword>
<keyword>ncut</keyword>
+ <keyword>ninversion</keyword>
<keyword>nlapply</keyword>
<keyword>ndestruct</keyword>
<keyword>Type[2]</keyword>
<keyword>CProp[2]</keyword>
</context>
+ <context id="quantifiers" style-ref="quantifiers">
+ <!-- quantifiers -->
+ <match>∀|∃|λ|=|→|⇒|…|≝|≡|\?</match>
+ </context>
+ <context id="tinycals" style-ref="tinycals">
+ <match>\[|\||\]|\{|\}|@|\$|#|\\\\|;|\.|:>|:</match>
+ </context>
</include>
</context>
</definitions>
-
-<!--
- <pattern-item _name = "Command [" style = "Keyword">
- <regex>\[</regex>
- </pattern-item>
- <pattern-item _name = "Command |" style = "Keyword">
- <regex>\|</regex>
- </pattern-item>
- <pattern-item _name = "Command ]" style = "Keyword">
- <regex>\]</regex>
- </pattern-item>
- <pattern-item _name = "Command {" style = "Keyword">
- <regex>\{</regex>
- </pattern-item>
- <pattern-item _name = "Command }" style = "Keyword">
- <regex>\}</regex>
- </pattern-item>
- <pattern-item _name = "Notation ast mark" style = "Keyword">
- <regex>@</regex>
- </pattern-item>
- <pattern-item _name = "Notation meta mark" style = "Keyword">
- <regex>\$</regex>
- </pattern-item>
-
-
- <keyword-list _name = "Whelp Macro" style = "Others 3"
- case-sensitive="TRUE"
- beginning-regex="whelp *"
- match-empty-string-at-beginning="FALSE"
- match-empty-string-at-end="FALSE" >
- <keyword>elim</keyword>
- <keyword>hint</keyword>
- <keyword>instance</keyword>
- <keyword>locate</keyword>
- <keyword>match</keyword>
- </keyword-list>
-
- <keyword-list _name = "TeX Macro" style = "Preprocessor"
- case-sensitive="TRUE"
- beginning-regex="\\"
- match-empty-string-at-beginning="FALSE"
- match-empty-string-at-end="FALSE" >
- <keyword>def</keyword>
- <keyword>forall</keyword>
- <keyword>lambda</keyword>
- <keyword>to</keyword>
- <keyword>exists</keyword>
- <keyword>Rightarrow</keyword>
- <keyword>Assign</keyword>
- <keyword>land</keyword>
- <keyword>lor</keyword>
- <keyword>lnot</keyword>
- <keyword>liff</keyword>
- <keyword>subst</keyword>
- <keyword>vdash</keyword>
- <keyword>iforall</keyword>
- <keyword>iexists</keyword>
- </keyword-list>
- -->
</language>