diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-08-24 17:36:27 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-08-24 17:36:27 +0000 |
| commit | c0b484e5ea6118b43e459190c02cc5a4261d0328 (patch) | |
| tree | 81dda7669a5b0266aec877571e1cd8d01a42a12e /plugins/extraction/table.mli | |
| parent | a3e890a390e9541045b1ce4c024fffcca275ff90 (diff) | |
Better highlighting of strings in coqide.
Strings were not highlighted out of comments. This would lead to funny
result, like certain strings (i.e. "(*") to cause all following code to be
highlighted as a string.
I've added strings in three different contexts (the same where comments
are highlighted). I think it's safe to do, I don't know if it's the best way,
though. In particular I don't know if it's the best way to highlight notations.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15761 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/extraction/table.mli')
0 files changed, 0 insertions, 0 deletions