diff options
| author | François Pottier <francois.pottier@inria.fr> | 2015-10-23 13:08:56 +0200 |
|---|---|---|
| committer | François Pottier <francois.pottier@inria.fr> | 2015-10-23 13:08:56 +0200 |
| commit | 8fee5abd0a1d0865d3d3d4b4de48aacb4be0914e (patch) | |
| tree | 971f13cd24e2c6e7ce653614897fcc9820caef59 /cparser/Lexer.mll | |
| parent | 883ebf950a4ef38788792cb1129fb9c408225ad3 (diff) | |
| download | compcert-kvx-8fee5abd0a1d0865d3d3d4b4de48aacb4be0914e.tar.gz compcert-kvx-8fee5abd0a1d0865d3d3d4b4de48aacb4be0914e.zip | |
Lexer cleanup: isolate the entry point into the lexer.
Diffstat (limited to 'cparser/Lexer.mll')
| -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 aca1be27..c453b15b 100644 --- a/cparser/Lexer.mll +++ b/cparser/Lexer.mll @@ -440,15 +440,19 @@ and singleline_comment = parse open Parser open Aut.GramDefs + (* This is the main entry point to the lexer. *) + + let lexer : lexbuf -> Pre_parser.token = + fun lexbuf -> + if lexbuf.lex_curr_p.pos_cnum = lexbuf.lex_curr_p.pos_bol then + initial_linebegin lexbuf + else + initial lexbuf + let tokens_stream filename text : token coq_Stream = let tokens = Queue.create () in let lexer_wraper lexbuf : Pre_parser.token = - let res = - if lexbuf.lex_curr_p.pos_cnum = lexbuf.lex_curr_p.pos_bol then - initial_linebegin lexbuf - else - initial lexbuf - in + let res = lexer lexbuf in Queue.push res tokens; res in |