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 /kernel/subtyping.ml | |
| 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.
Diffstat (limited to 'kernel/subtyping.ml')
0 files changed, 0 insertions, 0 deletions