From 8fee5abd0a1d0865d3d3d4b4de48aacb4be0914e Mon Sep 17 00:00:00 2001 From: François Pottier Date: Fri, 23 Oct 2015 13:08:56 +0200 Subject: Lexer cleanup: isolate the entry point into the lexer. --- cparser/Lexer.mll | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) (limited to 'cparser/Lexer.mll') 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 -- cgit