aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Lexer.mll
diff options
context:
space:
mode:
authorFrançois Pottier <francois.pottier@inria.fr>2015-10-23 13:11:23 +0200
committerFrançois Pottier <francois.pottier@inria.fr>2015-10-23 13:11:23 +0200
commitdca619cc34e64e63fe36ec9b5acdb42aafe665a8 (patch)
tree636b46bf5443045317730e544296d3949cdc53bc /cparser/Lexer.mll
parent8fee5abd0a1d0865d3d3d4b4de48aacb4be0914e (diff)
downloadcompcert-kvx-dca619cc34e64e63fe36ec9b5acdb42aafe665a8.tar.gz
compcert-kvx-dca619cc34e64e63fe36ec9b5acdb42aafe665a8.zip
Lexer cleanup: isolate [lexer_wraper] and rename it to [lexer].
Diffstat (limited to 'cparser/Lexer.mll')
-rw-r--r--cparser/Lexer.mll16
1 files changed, 10 insertions, 6 deletions
diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll
index c453b15b..ab4e03fe 100644
--- a/cparser/Lexer.mll
+++ b/cparser/Lexer.mll
@@ -449,17 +449,21 @@ and singleline_comment = parse
else
initial lexbuf
+ (* [lexer tokens buffer] is a new lexer, which wraps [lexer], and also
+ records the token stream into the FIFO queue [tokens]. *)
+
+ let lexer tokens : lexbuf -> Pre_parser.token =
+ fun lexbuf ->
+ let token = lexer lexbuf in
+ Queue.push token tokens;
+ token
+
let tokens_stream filename text : token coq_Stream =
let tokens = Queue.create () in
- let lexer_wraper lexbuf : Pre_parser.token =
- let res = lexer lexbuf in
- Queue.push res tokens;
- res
- in
let lexbuf = Lexing.from_string text in
lexbuf.lex_curr_p <- {lexbuf.lex_curr_p with pos_fname = filename; pos_lnum = 1};
contexts_stk := [init_ctx];
- Pre_parser.translation_unit_file lexer_wraper lexbuf;
+ Pre_parser.translation_unit_file (lexer tokens) lexbuf;
assert (List.length !contexts_stk = 1);
let rec compute_token_stream () =
let loop t v =