The standard library Winix_Pure_File_For_Os__Premicrothread api defines access to “pure” (side-effect free) input. (No attempt is made to implement pure output.)
Implementations of Winix_Pure_File_For_Os__Premicrothread are produced by winix_data_file_for_os_g__premicrothread and winix_text_file_for_os_g__premicrothread from respectively src/lib/std/src/io/winix-data-file-for-os-g–premicrothread.pkg and src/lib/std/src/io/winix-text-file-for-os-g–premicrothread.pkg.
Predefined packages generated by those two include the standard library winix_text_file_for_posix and winix_data_file_for_posix packages, more commonly referenced by the synonymous packages file and data_file.
The Winix_Pure_File_For_Os__Premicrothread api source code is in src/lib/std/src/io/winix-pure-file-for-os–premicrothread.api.
See also: Winix_Pure_File_For_Os.
See also: pur ("pure_io").
See also: Winix_File_For_Os__Premicrothread. The above information is manually maintained and may contain errors.
api { Vector; Element; Filereader; Filewriter; Input_Stream; Output_Stream; File_Position; Out_Position; make_instream : (Filereader , 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); close_input : Input_Stream -> Void; end_of_stream : Input_Stream -> Bool; get_reader : Input_Stream -> (Filereader , Vector); file_position_in : Input_Stream -> File_Position; make_outstream : (Filewriter , io_exceptions::Buffering_Mode) -> Output_Stream; write : (Output_Stream , Vector) -> Void; write_one : (Output_Stream , Element) -> Void; flush : Output_Stream -> Void; close_output : Output_Stream -> Void; set_buffering_mode : (Output_Stream , io_exceptions::Buffering_Mode) -> Void; get_buffering_mode : Output_Stream -> io_exceptions::Buffering_Mode; get_writer : Output_Stream -> (Filewriter , io_exceptions::Buffering_Mode); file_pos_out : Out_Position -> File_Position; get_output_position : Output_Stream -> Out_Position; set_output_position : Out_Position -> Void;};