diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-09-17 16:12:17 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-09-17 16:14:03 +0200 |
| commit | 55855391401e7476ea55e7b13cce3f15b32d9d8e (patch) | |
| tree | 5b141f7648015f0e34191332cff7c859328d8e7f | |
| parent | 00d4c83968f17bb302af61d6fa9160c944e68b29 (diff) | |
Fix ambiguous regex in syntax highlighting.
This fix considerably speeds up syntax highlighting. It also avoids burning
100% CPU when typing long identifiers. Finally, identifiers longer than 20
characters are now properly highlighted, since the stack of the automaton
no longer overflows because of them.
| -rw-r--r-- | ide/coq.lang | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/coq.lang b/ide/coq.lang index 656041d30..2905b26f0 100644 --- a/ide/coq.lang +++ b/ide/coq.lang @@ -26,7 +26,7 @@ <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="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> |