diff options
| -rw-r--r-- | cparser/Lexer.mll | 4 | ||||
| -rw-r--r-- | cparser/Parse.ml | 18 |
2 files changed, 17 insertions, 5 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; diff --git a/cparser/Parse.ml b/cparser/Parse.ml index cfa95688..1d92d5a5 100644 --- a/cparser/Parse.ml +++ b/cparser/Parse.ml @@ -38,9 +38,22 @@ let parse_transformations s = s; !t +let read_file sourcefile = + let ic = open_in sourcefile in + let n = in_channel_length ic in + let text = really_input_string ic n in + close_in ic; + text + let preprocessed_file transfs name sourcefile = Cerrors.reset(); - let ic = open_in sourcefile in + (* Reading the whole file at once may seem costly, but seems to be + the simplest / most robust way of accessing the text underlying + a range of positions. This is used when printing an error message. + Plus, I note that reading the whole file into memory leads to a + speed increase: "make -C test" speeds up by 3 seconds out of 40 + on my machine. *) + let text = read_file sourcefile in let p = try let t = parse_transformations transfs in @@ -52,7 +65,7 @@ let preprocessed_file transfs name sourcefile = parsing of the entire file. This is non-negligeabe, so we cannot use Timing.time2 *) (fun () -> - Parser.translation_unit_file inf (Lexer.tokens_stream name ic)) () + Parser.translation_unit_file inf (Lexer.tokens_stream name text)) () with | Parser.Parser.Inter.Fail_pr -> (* Theoretically impossible : implies inconsistencies @@ -65,5 +78,4 @@ let preprocessed_file transfs name sourcefile = with | Cerrors.Abort -> [] in - close_in ic; if Cerrors.check_errors() then None else Some p |