diff options
| author | Pierre-Marie Pédrot | 2014-08-28 11:41:37 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-08-28 11:41:37 +0200 |
| commit | ebcee1bf76fe47efc93efc7d7cbd5371db3bb368 (patch) | |
| tree | 427ebdc6caafe7a09617cba7cb8ae06464f6edab /lib | |
| parent | ddc4d94e9fc45f1aa058c52bba8d914048592153 (diff) | |
Fixing bug #3541.
All superscript numbers are now symbols instead of parts of identifiers.
This disallows some identifiers, but hopefully not a lot of people were
using superscripts as part of identifiers, weren't they?
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/unicode.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/lib/unicode.ml b/lib/unicode.ml index f26af10141..0764531c1a 100644 --- a/lib/unicode.ml +++ b/lib/unicode.ml @@ -102,7 +102,10 @@ let classify = (* Exceptions (from a previous version of this function). *) mk_lookup_table_from_unicode_tables_for Symbol [ - single 0x000B2; (* Squared. *) + [(0x000B2, 0x000B3)]; (* Superscript 2-3. *) + single 0x000B9; (* Superscript 1. *) + single 0x02070; (* Superscript 0. *) + [(0x02074, 0x02079)]; (* Superscript 4-9. *) single 0x0002E; (* Dot. *) ]; mk_lookup_table_from_unicode_tables_for Letter |