Class STD_FILES

-- Default output

-- Standard error file

-- Standard input file

-- Standard output file

-- Return the default_output or output
-- if default_output is Void.
--| Useful if a class inherits from STD_FILES and
--| and a putint is applied without standard setting.

-- Last character read by read_character

-- Last double read by read_double

-- Last integer read by read_integer

-- Last 16-bit integer read by read_integer_16

-- Last integer read by read_integer

-- Last 8-bit integer read by read_integer_64

-- Last 8-bit integer read by read_integer_8

-- Last 32-bit natural read by read_natural_32

-- Last 16-bit natural read by read_natural_16

-- Last 32-bit natural read by read_natural_32

-- Last 64-bit natural read by read_natural_64

-- Last 8-bit natural read by read_natural_8

-- Last real read by read_real

-- Last string read by read_line,
-- read_stream, or read_word

-- Last character read by read_character

-- Last double read by read_double

-- Last integer read by read_integer

-- Last real read by read_real

-- Last string read by read_line,
-- read_stream, or read_word

-- Write line feed at end of default output.

-- Write b at end of default output.

-- Write c at end of default output.

-- Write d at end of default output.

-- Write i at end of default output.

-- Write i at end of default output.

-- Write i at end of default output.

-- Write i at end of default output.

-- Write i at end of default output.

-- Write i at end of default output.

-- Write i at end of default output.

-- Write i at end of default output.

-- Write i at end of default output.

-- Write i at end of default output.

-- Write line feed at end of default output.

-- Write r at end of default output.

-- Write s at end of default output.

-- Write b at end of default output.

-- Write c at end of default output.

-- Write d at end of default output.

-- Write i at end of default output.

-- Write r at end of default output.

-- Write s at end of default output.

-- Use standard error as default output.

-- Use f as default output.

-- Use standard output as default output.

-- Move to next input line on standard input.

-- Read a new character from standard input.
-- It will not return until read operation is
-- terminated when enter key is pressed.
-- Make result available in last_character.
-- last_character will also contains platform
-- specific newline character.

-- Read a new double from standard input.
-- Make result available in last_double.

-- Read a new 32-bit integer from standard input.
-- Make result available in last_integer.

-- Read a new 16-bit integer from standard input.
-- Make result available in last_integer_16.

-- Read a new 32-bit integer from standard input.
-- Make result available in last_integer.

-- Read a new 64-bit integer from standard input.
-- Make result available in last_integer_64.

-- Read a new 8-bit integer from standard input.
-- Make result available in last_integer_8.

-- Read a line from standard input.
-- Make result available in last_string.

-- Read a new 32-bit natural from standard input.
-- Make result available in last_natural.

-- Read a new 16-bit natural from standard input.
-- Make result available in last_natural_16.

-- Read a new 32-bit natural from standard input.
-- Make result available in last_natural.

-- Read a new 64-bit natural from standard input.
-- Make result available in last_natural_64.

-- Read a new 8-bit natural from standard input.
-- Make result available in last_natural_8.

-- Read a new real from standard input.
-- Make result available in last_real.

-- Read a string of at most nb_char bound characters
-- from standard input.
-- Make result available in last_string.

-- Read a new word from standard input.
-- Make result available in last_string.

-- Read a new character from standard input.
-- It will not return until read operation is
-- terminated when enter key is pressed.
-- Make result available in last_character.
-- last_character will also contains platform
-- specific newline character.

-- Read a new double from standard input.
-- Make result available in last_double.

-- Read a new 32-bit integer from standard input.
-- Make result available in last_integer.

-- Read a line from standard input.
-- Make result available in last_string.

-- Read a new real from standard input.
-- Make result available in last_real.

-- Read a string of at most nb_char bound characters
-- from standard input.
-- Make result available in last_string.

-- Read a new word from standard input.
-- Make result available in last_string.

-- Move to next input line on standard input.