rendered paste body(* File input handling *)
structure Read_Input : READ_INPUT =
struct
(* line number, contents of the line *)
type lineinput = {line: int, contents: char list};
(* File name, and a list of line descriptors *)
type file_input_stream = {filename: string, lines: lineinput list};
fun input_file (a : string) =
let
val inputstream = TextIO.openIn a;
fun input_lines (stream : TextIO.instream, linenum : int) =
if TextIO.endOfStream(stream) then (TextIO.closeIn stream; nil)
else
{line = linenum, contents = (explode (TextIO.inputLine stream))}::input_lines (stream, linenum + 1);
in
{filename = a, lines = (input_lines (inputstream, 1))}
end;
end;
type lineinput = {line: int, contents: char list};
type file_input_stream = {filename: string, lines: lineinput list};