diff options
Diffstat (limited to 'ide/coq.lang')
-rw-r--r-- | ide/coq.lang | 59 |
1 files changed, 32 insertions, 27 deletions
diff --git a/ide/coq.lang b/ide/coq.lang index 608a4aea..65150d6a 100644 --- a/ide/coq.lang +++ b/ide/coq.lang @@ -22,19 +22,19 @@ </styles> <definitions> - <define-regex id="space">\s</define-regex> + <define-regex id="space">\s+</define-regex> <define-regex id="first_ident_char">[_\p{L}]</define-regex> <define-regex id="ident_char">[_\p{L}'\pN]</define-regex> <define-regex id="ident">\%{first_ident_char}\%{ident_char}*</define-regex> <define-regex id="qualit">(\%{ident}\.)*\%{ident}</define-regex> <define-regex id="undotted_sep">[-+*{}]</define-regex> <define-regex id="dot_sep">\.(\s|\z)</define-regex> - <define-regex id="single_decl">(Definition)|(Let)|(Example)|(SubClass)|(Fixpoint)|(CoFixpoint)|(Scheme)|(Function)|(Hypothesis)|(Axiom)|(Variable)|(Parameter)|(Conjecture)|(Inductive)|(CoInductive)|(Record)|(Structure)|(Ltac)|(Instance)|(Context)|(Class)|(Module(\%{space}+Type)?)|(Existing\%{space}+Instance)|(Canonical\%{space}+Structure)</define-regex> - <define-regex id="mult_decl">(Hypotheses)|(Axioms)|(Variables)|(Parameters)|(Implicit\%{space}+Type(s)?)</define-regex> - <define-regex id="locality">(((Local)|(Global))\%{space}+)?</define-regex> - <define-regex id="begin_proof">(Theorem)|(Lemma)|(Fact)|(Remark)|(Corollary)|(Proposition)|(Property)</define-regex> - <define-regex id="end_proof">(Qed)|(Defined)|(Admitted)|(Abort)</define-regex> - <define-regex id="decl_head">((?'gal'\%{locality}(Program\%{space}+)?(\%{single_decl}|\%{begin_proof}))\%{space}+(?'id'\%{ident}))|((?'gal4list'\%{mult_decl})(?'id_list'(\%{space}+\%{ident})*))|(?'gal2'Goal)</define-regex> + <define-regex id="single_decl">Definition|Let|Example|SubClass|(Co)?Fixpoint|Function|Conjecture|(Co)?Inductive|Record|Structure|Ltac|Instance|Class|Existing\%{space}Instance|Canonical\%{space}Structure|Coercion</define-regex> + <define-regex id="mult_decl">Hypothes[ie]s|Axiom(s)?|Variable(s)?|Parameter(s)?|Context|Implicit\%{space}Type(s)?</define-regex> + <define-regex id="locality">((Local|Global)\%{space})?</define-regex> + <define-regex id="begin_proof">Theorem|Lemma|Fact|Remark|Corollary|Proposition|Property</define-regex> + <define-regex id="end_proof">Qed|Defined|Admitted|Abort|Save</define-regex> + <define-regex id="decl_head">((?'gal'\%{locality}(Program\%{space})?(\%{single_decl}|\%{begin_proof}))\%{space}(?'id'\%{ident}))|((?'gal4list'\%{mult_decl})(?'id_list'(\%{space}\%{ident})*))|(?'gal2'Goal)</define-regex> <context id="escape-seq" style-ref="escape"> <match>""</match> @@ -97,7 +97,6 @@ <keyword>then</keyword> <keyword>else</keyword> <keyword>return</keyword> - <keyword>using</keyword> </context> <context id="constr-sort" style-ref="constr-sort"> <keyword>Prop</keyword> @@ -113,7 +112,7 @@ </include> </context> <context id="proof"> - <start>Proof(\%{dot_sep}|\%{space}+(using)|\%{space}+(with))</start> + <start>Proof(\%{dot_sep}|\%{space}using|\%{space}with)</start> <end>\%{end_proof}\%{dot_sep}</end> <include> <context sub-pattern="0" where="start" style-ref="vernac-keyword"/> @@ -157,17 +156,18 @@ <keyword>Eval</keyword> <keyword>Load</keyword> <keyword>Undo</keyword> + <keyword>(Print|Reset)\%{space}+Extraction\%{space}+(Inline|Blacklist)</keyword> <keyword>Print</keyword> - <keyword>Save</keyword> <keyword>Comments</keyword> - <keyword>Solve\%{space}+Obligation</keyword> - <keyword>((Uns)|(S))et(\%{space}+\%{ident})+</keyword> - <keyword>(\%{locality}|((Reserved)|(Tactic))\%{space}+)?Notation</keyword> + <keyword>Solve\%{space}Obligation</keyword> + <keyword>(Uns|S)et(\%{space}\%{ident})+</keyword> + <keyword>(\%{locality}|(Reserved|Tactic)\%{space})?Notation</keyword> <keyword>\%{locality}Infix</keyword> - <keyword>(Print)|(Reset)\%{space}+Extraction\%{space}+(Inline)|(Blacklist)</keyword> + <keyword>Declare\%{space}ML\%{space}Module</keyword> + <keyword>Extraction\%{space}Language\%{space}(Ocaml|Haskell|Scheme|JSON)</keyword> </context> <context id="hint-command" style-ref="vernac-keyword"> - <prefix>\%{locality}Hint\%{space}+</prefix> + <prefix>\%{locality}Hint\%{space}</prefix> <keyword>Resolve</keyword> <keyword>Immediate</keyword> <keyword>Constructors</keyword> @@ -178,35 +178,40 @@ <keyword>Rewrite</keyword> </context> <context id="scope-command" style-ref="vernac-keyword"> - <suffix>\%{space}+Scope</suffix> + <suffix>\%{space}Scope</suffix> <keyword>\%{locality}Open</keyword> <keyword>\%{locality}Close</keyword> <keyword>Bind</keyword> <keyword>Delimit</keyword> </context> <context id="command-for-qualit"> - <suffix>\%{space}+(?'qua'\%{qualit})</suffix> + <suffix>\%{space}(?'qua'\%{qualit})</suffix> <keyword>Chapter</keyword> - <keyword>Combined\%{space}+Scheme</keyword> + <keyword>Combined\%{space}Scheme</keyword> + <keyword>Scheme\%{space}(Induction|Minimality|Elimination|Case|Equality)\%{space}for</keyword> <keyword>End</keyword> <keyword>Section</keyword> + <keyword>Module(\%{space}Type)?</keyword> + <keyword>Declare\%{space}Module(\%{space}(Import|Export))?</keyword> + <keyword>About</keyword> <keyword>Arguments</keyword> - <keyword>Implicit\%{space}+Arguments</keyword> - <keyword>Import</keyword> + <keyword>Implicit\%{space}Arguments</keyword> <keyword>Include</keyword> - <keyword>Export</keyword> - <keyword>Require(\%{space}+((Import)|(Export)))?</keyword> - <keyword>(Recursive\%{space}+)?Extraction(\%{space}+(Language\%{space}+(Ocaml)|(Haskell)|(Scheme)|(Toplevel))|(Library)|((No)?Inline)|(Blacklist))?</keyword> - <keyword>Extract\%{space}+(Inlined\%{space}+)?(Constant)|(Inductive)</keyword> + <keyword>Extract\%{space}((Inlined\%{space})?Constant|Inductive)</keyword> <include> <context sub-pattern="1" style-ref="vernac-keyword"/> <context sub-pattern="qua" style-ref="identifier"/> </include> </context> - <context id="command-for-qualit-list" style-ref="vernac-keyword"> - <suffix>(?'qua_list'(\%{space}+\%{qualit})+)</suffix> - <keyword>Typeclasses (Transparent)|(Opaque)</keyword> + <context id="command-for-qualit-list"> + <suffix>(?'qua_list'(\%{space}\%{qualit})+)</suffix> + <keyword>Typeclasses (Transparent|Opaque)</keyword> + <keyword>Require(\%{space}(Import|Export))?</keyword> + <keyword>Import</keyword> + <keyword>Export</keyword> + <keyword>((Recursive|Separate)\%{space})?Extraction(\%{space}(Library|(No)?Inline|Blacklist))?</keyword> <include> + <context sub-pattern="1" style-ref="vernac-keyword"/> <context sub-pattern="qua_list" style-ref="identifier"/> </include> </context> |