diff options
| author | François Pottier <francois.pottier@inria.fr> | 2015-10-16 17:56:06 +0200 |
|---|---|---|
| committer | François Pottier <francois.pottier@inria.fr> | 2015-10-23 11:32:28 +0200 |
| commit | 03f39523094fd41c8aad5ee7a8169ffc448cfd4a (patch) | |
| tree | f59f6951f244261d8ef38a77860f6feff33a4880 /cparser/Lexer.mll | |
| parent | e036d68cb41de1ddac47d7686d25904281405ffe (diff) | |
| download | compcert-kvx-03f39523094fd41c8aad5ee7a8169ffc448cfd4a.tar.gz compcert-kvx-03f39523094fd41c8aad5ee7a8169ffc448cfd4a.zip | |
Read the whole source C file into memory instad of reading it on demand.
Having the file in memory will help build an error message.
Also, this may be slightly faster.
Diffstat (limited to 'cparser/Lexer.mll')
| -rw-r--r-- | cparser/Lexer.mll | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll index 6be59aa8..aca1be27 100644 --- a/cparser/Lexer.mll +++ b/cparser/Lexer.mll @@ -440,7 +440,7 @@ and singleline_comment = parse open Parser open Aut.GramDefs - let tokens_stream filename channel : token coq_Stream = + let tokens_stream filename text : token coq_Stream = let tokens = Queue.create () in let lexer_wraper lexbuf : Pre_parser.token = let res = @@ -452,7 +452,7 @@ and singleline_comment = parse Queue.push res tokens; res in - let lexbuf = Lexing.from_channel channel 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; |