diff options
Diffstat (limited to 'src/pre_lexer.mll')
| -rw-r--r-- | src/pre_lexer.mll | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/pre_lexer.mll b/src/pre_lexer.mll index f648a594..3c308b99 100644 --- a/src/pre_lexer.mll +++ b/src/pre_lexer.mll @@ -9,6 +9,14 @@ (* Robert Norton-Wright *) (* Christopher Pulte *) (* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) (* *) (* All rights reserved. *) (* *) @@ -118,7 +126,7 @@ let binarydigit = ['0'-'1'] let hexdigit = ['0'-'9''A'-'F''a'-'f'] let alphanum = letter|digit let startident = letter|'_' -let ident = alphanum|['_''\''] +let ident = alphanum|['_''\'''#'] let tyvar_start = '\'' let oper_char = ['!''$''%''&''*''+''-''.''/'':''<''=''>''?''@''^''|''~'] let escape_sequence = ('\\' ['\\''\"''\'''n''t''b''r']) | ('\\' digit digit digit) | ('\\' 'x' hexdigit hexdigit) |