diff options
| author | Arnaud Spiwack | 2015-06-25 18:01:23 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2015-06-25 18:01:23 +0200 |
| commit | 42b7e36ddb68f53ada686900e5a98435d9ff7fde (patch) | |
| tree | 886293cf052b3e5e16aefbac4c14d600dfb7b0fa | |
| parent | 28855216037570aeabc544ab232bb896d7a7327f (diff) | |
Add coqide syntax highlighting for `Assume`.
| -rw-r--r-- | ide/coq.lang | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/ide/coq.lang b/ide/coq.lang index c65432bdb7..a31eadc707 100644 --- a/ide/coq.lang +++ b/ide/coq.lang @@ -29,12 +29,13 @@ <define-regex id="qualit">(\%{ident}\.)*\%{ident}</define-regex> <define-regex id="dot_sep">\.(\s|\z)</define-regex> <define-regex id="bullet">([-+*]+|{)(\s|\z)|}(\s*})*</define-regex> + <define-regex id="assume">(?'gal0'Assume)\%{space}\[\%{ident}*\]\%{space}</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> + <define-regex id="decl_head">((\%{assume})?(?'gal'\%{locality}(Program\%{space})?(\%{single_decl}|\%{begin_proof}))\%{space}(?'id'\%{ident}))|((?'gal4list'\%{mult_decl})(?'id_list'(\%{space}\%{ident})*))|(?'gal2'Goal)</define-regex> <!-- Strings, with '""' an escape sequence --> <context id="string" style-ref="string" class="string"> @@ -106,6 +107,7 @@ <end>\%{dot_sep}</end> <include> <context sub-pattern="id" where="start" style-ref="identifier"/> + <context sub-pattern="gal0" where="start" style-ref="gallina-keyword"/> <context sub-pattern="gal" where="start" style-ref="gallina-keyword"/> <context sub-pattern="gal2" where="start" style-ref="gallina-keyword"/> <context sub-pattern="id_list" where="start" style-ref="identifier"/> |