The standard library Imperative_Io api defines access to traditional imperative-style file I/O (as opposed to applicative — side-effect-free — I/O).
The Imperative_Io api is include-ed by src/lib/std/src/io/binary-io.api.
The Imperative_Io api source code is in src/lib/std/src/io/imperative-io.api.
See also: Pure_Io.
The above information is manually maintained and may contain errors.
api {
Vector ;
Element ;
Input_Stream ;
Output_Stream ;
read : Input_Stream -> Vector;
read_one : Input_Stream -> Null_Or(Element );
read_n : (Input_Stream , Int) -> Vector;
read_all : Input_Stream -> Vector;
can_read : (Input_Stream , Int) -> Null_Or(Int );
lookahead : Input_Stream -> Null_Or(Element );
close_input : Input_Stream -> Void;
end_of_stream : Input_Stream -> Bool;
write : (Output_Stream , Vector) -> Void;
write_one : (Output_Stream , Element) -> Void;
flush : Output_Stream -> Void;
close_output : Output_Stream -> Void;
package pure_io : api {
Vector ;
Element ;
Reader ;
Writer ;
Input_Stream ;
Output_Stream ;
File_Position ;
Out_Position ;
make_instream : (Reader , Vector) -> Input_Stream;
read : Input_Stream -> (Vector , Input_Stream);
read_one : Input_Stream -> Null_Or(((Element , Input_Stream)) );
read_n : (Input_Stream , Int) -> (Vector , Input_Stream);
read_all : Input_Stream -> (Vector , Input_Stream);
can_read : (Input_Stream , Int) -> Null_Or(Int );
close_input : Input_Stream -> Void;
end_of_stream : Input_Stream -> Bool;
get_reader : Input_Stream -> (Reader , Vector);
file_position_in : Input_Stream -> File_Position;
make_outstream : (Writer , io_exceptions::Buffering) -> Output_Stream;
write : (Output_Stream , Vector) -> Void;
write_one : (Output_Stream , Element) -> Void;
flush : Output_Stream -> Void;
close_output : Output_Stream -> Void;
set_buffer_mode : (Output_Stream , io_exceptions::Buffering) -> Void;
get_buffer_mode : Output_Stream -> io_exceptions::Buffering;
get_writer : Output_Stream -> (Writer , io_exceptions::Buffering);
file_pos_out : Out_Position -> File_Position;
get_output_position : Output_Stream -> Out_Position;
set_output_position : Out_Position -> Void;
};;
make_instream : pure_io::Input_Stream -> Input_Stream;
get_instream : Input_Stream -> pure_io::Input_Stream;
set_instream : (Input_Stream , pure_io::Input_Stream) -> Void;
get_output_position : Output_Stream -> pure_io::Out_Position;
set_output_position : (Output_Stream , pure_io::Out_Position) -> Void;
make_outstream : pure_io::Output_Stream -> Output_Stream;
get_outstream : Output_Stream -> pure_io::Output_Stream;
set_outstream : (Output_Stream , pure_io::Output_Stream) -> Void;
sharing pure_io::Element = Element
sharing pure_io::Vector = Vector
};