diff options
author | François Pottier <francois.pottier@inria.fr> | 2015-10-23 13:11:23 +0200 |
---|---|---|
committer | François Pottier <francois.pottier@inria.fr> | 2015-10-23 13:11:23 +0200 |
commit | dca619cc34e64e63fe36ec9b5acdb42aafe665a8 (patch) | |
tree | 636b46bf5443045317730e544296d3949cdc53bc /cparser | |
parent | 8fee5abd0a1d0865d3d3d4b4de48aacb4be0914e (diff) | |
download | compcert-dca619cc34e64e63fe36ec9b5acdb42aafe665a8.tar.gz compcert-dca619cc34e64e63fe36ec9b5acdb42aafe665a8.zip |
Lexer cleanup: isolate [lexer_wraper] and rename it to [lexer].
Diffstat (limited to 'cparser')
-rw-r--r-- | cparser/Lexer.mll | 16 |
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 = |