summaryrefslogtreecommitdiff
path: root/src/lexer.mll
diff options
context:
space:
mode:
authorThomas Bauereiss2017-12-06 17:18:36 +0000
committerThomas Bauereiss2017-12-06 17:18:36 +0000
commit2bc281428a3a1d608d56f69e71b50056a25e3da0 (patch)
treedfd8e8a13702696fd9daef64315952b9652f95e8 /src/lexer.mll
parentc3c3c40a1d4f81448d8356317e88be2b04363df7 (diff)
parent44e9396fa90ab68ee4c8d9674c6bbad6fc851c6d (diff)
Merge remote branch 'experiments' into experiments
Diffstat (limited to 'src/lexer.mll')
-rw-r--r--src/lexer.mll10
1 files changed, 9 insertions, 1 deletions
diff --git a/src/lexer.mll b/src/lexer.mll
index 3b1a1583..35ab6627 100644
--- a/src/lexer.mll
+++ b/src/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. *)
(* *)
@@ -157,7 +165,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)