aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdoc/cpretty.mll
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-10-29 11:59:13 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-10-29 11:59:13 +0000
commit5893703b77fb17885fd66dbf575b9533cbf96a90 (patch)
treec401c0607604b56a1360e4fdae3304d521c9bfe3 /tools/coqdoc/cpretty.mll
parent62ddbf4c06974bb701dd6b370c6b4d670cb5d7cd (diff)
Fixed broken globalization of identifiers containing utf8 letters
without knowing it. Note: location tables have grown a lot, a better representation of the contents of the glob files in coqdoc might improve efficiency. Also added keywords. Information is now obtained from the glob file to know the exact span of identifiers. Kept a class of identifiers (and enriched them) for the main purpose of distinguishing between idents and symbols in the absence of a glob file. Still a lot of work to do in coqdoc to make it more robust... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14624 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/coqdoc/cpretty.mll')
-rw-r--r--tools/coqdoc/cpretty.mll2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 65a232b4a..89047e83c 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -276,7 +276,7 @@ let firstchar =
(* '\206' ([ '\145' - '\183'] | '\187') | *)
(* '\xCF' [ '\x00' - '\xCE' ] | *)
(* utf-8 letterlike symbols *)
- '\206' ('\160' | [ '\177'-'\183'] | '\187') |
+ '\206' (['\145'-'\161'] | ['\163'-'\187']) |
'\226' ('\130' [ '\128'-'\137' ] (* subscripts *)
| '\129' [ '\176'-'\187' ] (* superscripts *)
| '\132' ['\128'-'\191'] | '\133' ['\128'-'\143'])