diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-02 08:03:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-02 08:03:05 +0200 |
| commit | 97adfc372fd716c6701677b69950cd9279f46f27 (patch) | |
| tree | 0f0b23f778074065d8920a9c55db81d36d854833 /ide | |
| parent | 54277abbf0fa15e0437d2a68859ceeef09ec70c3 (diff) | |
| parent | bd5da52c6c625cb4559dd92051384383473ecb1b (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coq.lang | 59 | ||||
| -rw-r--r-- | ide/coq.png | bin | 71924 -> 12907 bytes |
2 files changed, 37 insertions, 22 deletions
diff --git a/ide/coq.lang b/ide/coq.lang index e25eedbca..484264ece 100644 --- a/ide/coq.lang +++ b/ide/coq.lang @@ -95,11 +95,24 @@ <keyword>Type</keyword> </context> - <context id="coq" class="no-spell-check"> + <!-- Terms --> + <context id="constr"> <include> <context ref="string"/> <context ref="coqdoc"/> <context ref="comment"/> + <context ref="constr-sort"/> + <context ref="constr-keyword"/> + <context id="dot-nosep"> + <match>\.\.</match> + </context> + </include> + </context> + + <context id="coq" class="no-spell-check"> + <include> + <context ref="coqdoc"/> + <context ref="comment"/> <context id="declaration"> <start>\%{decl_head}</start> @@ -110,14 +123,7 @@ <context sub-pattern="gal2" where="start" style-ref="gallina-keyword"/> <context sub-pattern="id_list" where="start" style-ref="identifier"/> <context sub-pattern="gal4list" where="start" style-ref="gallina-keyword"/> - <context ref="constr-keyword"/> - <context ref="constr-sort"/> - <context id="dot-nosep"> - <match>\.\.</match> - </context> - <context ref="string"/> - <context ref="coqdoc"/> - <context ref="comment"/> + <context ref="constr"/> </include> </context> @@ -127,21 +133,19 @@ <include> <context sub-pattern="0" where="start" style-ref="vernac-keyword"/> <context sub-pattern="0" where="end" style-ref="vernac-keyword"/> - <context ref="command-in-proof"/> - <context ref="string"/> <context ref="coqdoc"/> <context ref="comment"/> - <context ref="constr-keyword"/> - <context ref="constr-sort"/> - <context id="bullet" extend-parent="false"> - <match>\%{dot_sep}\s*(?'bul'\%{bullet})</match> + <context id="bullet" style-ref="vernac-keyword" extend-parent="false"> + <match>\%{bullet}</match> + </context> + <context extend-parent="false"> + <start>\%[</start> + <end>\%{dot_sep}</end> <include> - <context sub-pattern="bul" style-ref="vernac-keyword"/> + <context ref="command-in-proof"/> + <context ref="constr"/> </include> </context> - <context id="bullet-sol" style-ref="vernac-keyword"> - <match>^\s*\%{bullet}</match> - </context> </include> </context> @@ -150,11 +154,19 @@ <end>\%{dot_sep}</end> <include> <context sub-pattern="0" where="start" style-ref="vernac-keyword"/> - <context ref="constr-keyword"/> - <context ref="constr-sort"/> + <context ref="constr"/> </include> </context> + <context ref="command"/> + </include> + </context> + + <!-- Toplevel commands --> + <context id="command" extend-parent="false"> + <start>\%[</start> + <end>\%{dot_sep}</end> + <include> <context id="command-in-proof" style-ref="vernac-keyword"> <keyword>About</keyword> <keyword>Check</keyword> @@ -166,7 +178,7 @@ <keyword>Transparent</keyword> </context> - <context id="command" style-ref="vernac-keyword"> + <context id="toplevel-command" style-ref="vernac-keyword"> <keyword>Add</keyword> <keyword>Load</keyword> <keyword>(Print|Reset)\%{space}+Extraction\%{space}+(Inline|Blacklist)</keyword> @@ -228,7 +240,10 @@ <context sub-pattern="qua_list" style-ref="identifier"/> </include> </context> + + <context ref="constr"/> </include> </context> + </definitions> </language> diff --git a/ide/coq.png b/ide/coq.png Binary files differindex cccd5a9a1..136bfdd5f 100644 --- a/ide/coq.png +++ b/ide/coq.png |
