Commit 051dd7f7 authored by POTTIER Francois's avatar POTTIER Francois

Moved [read_whole_file] from [PreFront] to [IO].

parent ba990748
......@@ -77,3 +77,29 @@ let invoke command =
| _ ->
None
(* ------------------------------------------------------------------------- *)
(* [read_whole_file filename] reads the file [filename] in text mode and
returns its contents as a string. *)
let read_whole_file filename =
(* Open the file in text mode, so that (under Windows) CRLF is converted to LF.
This guarantees that one byte is one character and seems to be required in
order to report accurate positions. *)
let channel = open_in filename in
(* The standard library functions [pos_in] and [seek_in] do not work correctly
when CRLF conversion is being performed, so we abandon their use. (They were
used to go and extract the text of semantic actions.) Instead we load the
entire file into memory up front, and work with a string. *)
(* The standard library function [in_channel_length] does not work correctly
when CRLF conversion is being performed, so we do not use it to read the
whole file. And the standard library function [Buffer.add_channel] uses
[really_input] internally, so we cannot use it either. Bummer. *)
let s = exhaust channel in
close_in channel;
s
......@@ -28,3 +28,8 @@ val exhaust: in_channel -> string
val invoke: string -> string option
(* [read_whole_file filename] reads the file [filename] in text mode and
returns its contents as a string. *)
val read_whole_file: string -> string
open Printf
let read_whole_file filename =
(* Open the file in text mode, so that (under Windows) CRLF is converted to LF.
This guarantees that one byte is one character and seems to be required in
order to report accurate positions. *)
let channel = open_in filename in
(* The standard library functions [pos_in] and [seek_in] do not work correctly
when CRLF conversion is being performed, so we abandon their use. (They were
used to go and extract the text of semantic actions.) Instead we load the
entire file into memory up front, and work with a string. *)
(* The standard library function [in_channel_length] does not work correctly
when CRLF conversion is being performed, so we do not use it to read the
whole file. And the standard library function [Buffer.add_channel] uses
[really_input] internally, so we cannot use it either. Bummer. *)
let s = IO.exhaust channel in
close_in channel;
s
let load_partial_grammar filename =
let validExt = if Settings.coq then ".vy" else ".mly" in
if Filename.check_suffix filename validExt then
......@@ -30,7 +8,7 @@ let load_partial_grammar filename =
Error.error [] (sprintf "argument file names should end in %s. \"%s\" is not accepted." validExt filename);
try
let contents = read_whole_file filename in
let contents = IO.read_whole_file filename in
Error.file_contents := Some contents;
let lexbuf = Lexing.from_string contents in
lexbuf.Lexing.lex_curr_p <-
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment