Eiffeldoc: TEXT_FILE

is_connected implies path /= Void

Overview

Creation features

{ANY}

make

The new created object is not connected.
connect_to (new_path: ABSTRACT_STRING)

Open text file for reading.

Features

{ANY}

connect_to (new_path: ABSTRACT_STRING)

Open text file for reading.
disconnect

Try to disconnect the stream.
can_unread_character: BOOLEAN
end_of_input: BOOLEAN

end_of_input means the previous attempt in character reading failed because the end has been reached.
out_in_tagged_out_memory

Append terse printable representation of current object in tagged_out_memory.

filtered_read_character
filtered_unread_character
filtered_last_character: CHARACTER
filtered_read_line_in (str: STRING)
filtered_read_available_in (str: STRING, limit: INTEGER_32)

Limit reading to what the buffer contains.

filtered_descriptor: INTEGER_32

Find the descriptor of the terminal stream...
filtered_has_descriptor: BOOLEAN

True if the underlying terminal stream has a descriptor
filtered_stream_pointer: POINTER

Find the pointer of the terminal stream...
filtered_has_stream_pointer: BOOLEAN

True if the underlying terminal stream has a pointer

{FILE_TOOLS}

same_as (other: TEXT_FILE_READ): BOOLEAN

{INPUT_STREAM}

input_stream: POINTER

{}

make

The new created object is not connected.
text_file_read_open (path_pointer: POINTER): POINTER
io_fclose (stream: POINTER)

{ANY}

path: STRING

Not Void when connected to the corresponding file on the disk.
is_connected: BOOLEAN

Is this file connected to some file of the operating system?

{}

set_path (new_path: ABSTRACT_STRING)

{ANY}

descriptor: INTEGER_32

Some OS-dependent descriptor.
has_descriptor: BOOLEAN

True if that stream can be associated to some OS-meaningful descriptor.
can_disconnect: BOOLEAN

True if the stream can be safely disconnected (without data loss, etc.)
url: URL

The URL to this stream as resource

{}

url_memory: URL
new_url: URL

{STREAM_HANDLER}

stream_pointer: POINTER

Some Back-end-dependent pointer (FILE* in C, InputStream or OutputStream in Java)
has_stream_pointer: BOOLEAN

True if that stream can be associated to some Back-end-meaningful stream pointer.

{ANY}

event_exception: EVENT_DESCRIPTOR

{}

stream_exception: STREAM_EXCEPTION

{RECYCLING_POOL}

recycle

Do whatever needs to be done to free resources or recycle other objects when recycling this one

{}

dispose

Action to be executed just before garbage collection reclaims an object.

{}

sequencer_descriptor (file: POINTER): INTEGER_32

{ANY}

can_read_character: BOOLEAN

Note that this state is usually temporary.
can_read_line: BOOLEAN
valid_last_character: BOOLEAN

{ANY}

read_character

If read_character fail, end_of_input is set.
read_line_in (buffer: STRING)

Same job as read_line but storage is directly done in buffer.
read_available_in (buffer: STRING, limit: INTEGER_32)

Same job as read_available but storage is directly done in buffer.
unread_character
last_character: CHARACTER
detach

Shake off the filter.

filter: FILTER_INPUT_STREAM

The filter that uses this stream as backend

{ANY}

event_can_read: EVENT_DESCRIPTOR

{}

can_read: CAN_READ_DATA_FROM_STREAM

{ANY}

is_filtered: BOOLEAN

Skipping separators:

{ANY}

skip_separators

Skip all separators (see is_separator of class CHARACTER) and make the first non-separator available in last_character.
skip_separators_using (separators: STRING)

Same job as skip_separators using the separators set.
skip_remainder_of_line

Skip all the remainder of the line including the end of line delimiter itself.

To read one number at a time:

{ANY}

read_integer

Read an integer according to the Eiffel syntax.
last_integer: INTEGER_32

Last integer read using read_integer.
valid_last_integer: BOOLEAN

Was the last call to read_integer successful ?
last_real: REAL_64

Last real read with read_real.
valid_last_real: BOOLEAN

Was the last call to read_real successful ?
read_real

Read a REAL and make the result available in last_real.

To read one line or one word at a time:

{ANY}

last_string: STRING

Access to the unique common buffer to get for example the result computed by read_line, read_word, newline, etc.
read_line

Read a complete line ended by '%N' or end_of_input.%
read_available (limit: INTEGER_32)

Read as many characters as possible, as long as the stream does not block and up to the given limit.
read_word

Read a word using is_separator of class CHARACTER.
newline

Consume input until newline ('%N') is found.
reach_and_skip (keyword: STRING)

Try to skip enough characters in order to reach the keyword which is skipped too.

Other features:

{ANY}

read_word_using (separators: STRING)

Same job as read_word using separators.
read_tail_in (str: STRING)

Read all remaining character of the stream in str.

{}

io_getc (stream: POINTER): INTEGER_32
io_ungetc (byte: CHARACTER, stream: POINTER)
io_fread (buf: NATIVE_ARRAY[CHARACTER], size: INTEGER_32, stream: POINTER): INTEGER_32

return size read or 0 if end of input (-1 on error => exception ?)
eof: INTEGER_32

set_filter (a_filter: FILTER)

Used by the filter itself to get attached

connect_to (new_path: ABSTRACT_STRING)

effective procedure

{ANY}

Open text file for reading.

The stream is positioned at the beginning of the file.

require

not is_connected
not_malformed_path: not new_path.is_empty

ensure

is_connected implies not end_of_input
is_connected implies path.same_as(new_path.out)

disconnect

effective procedure

{ANY}

Try to disconnect the stream.

Note that it *does not* ensure that the stream will effectively be disconnected (some terminal streams, for instance, are always connected) but the feature can be used to "shake off" filters.

require

is_connected
can_disconnect

is_connected
can_disconnect

is_connected
can_disconnect

ensure

not is_filtered

can_unread_character: BOOLEAN

effective function

{ANY}

require

is_connected
valid_last_character

end_of_input: BOOLEAN

writable attribute

{ANY}

end_of_input means the previous attempt in character reading failed because the end has been reached.

So last_character is not valid and you are not allowed to do any read attempt anymore.

Notes:

Just after a successful connect, end_of_input is always False because you did not yet read anything).
Once the end of input has been reached, this is definitive in that no more characters will ever be provided (but of course you can still come back if can_unread_character; end_of_input will be changed if you unread_character). In that, it is different from can_read_character which is only a temporary state.

Please refer to the Liberty Eiffel FAQ or tutorial/io examples.

out_in_tagged_out_memory

effective procedure

{ANY}

Append terse printable representation of current object in tagged_out_memory.

require

locked: tagged_out_locked

locked: tagged_out_locked

locked: tagged_out_locked

ensure

still_locked: tagged_out_locked
not_cleared: tagged_out_memory.count >= old tagged_out_memory.count
append_only: old tagged_out_memory.twin.is_equal(tagged_out_memory.substring(1, old tagged_out_memory.count))

filtered_read_character

effective procedure

require

is_connected
can_read_character

filtered_unread_character

effective procedure

require

is_connected
can_unread_character

filtered_last_character: CHARACTER

writable attribute

require

is_connected
valid_last_character

filtered_read_line_in (str: STRING)

effective procedure

require

is_connected
str /= Void

filtered_read_available_in (str: STRING, limit: INTEGER_32)

effective procedure

Limit reading to what the buffer contains.

If the buffer is already exhausted, just fill it once.

require

is_connected
str /= Void

filtered_descriptor: INTEGER_32

effective function

Find the descriptor of the terminal stream...

Filters do not have descriptors of their own

require

is_connected
filtered_has_descriptor

is_connected
filtered_has_descriptor

is_connected
filtered_has_descriptor

filtered_has_descriptor: BOOLEAN

is True

constant attribute

True if the underlying terminal stream has a descriptor

require

is_connected

is_connected

is_connected

filtered_stream_pointer: POINTER

effective function

Find the pointer of the terminal stream...

Filters do not have pointers of their own

require

is_connected
filtered_has_stream_pointer

is_connected
filtered_has_stream_pointer

is_connected
filtered_has_stream_pointer

filtered_has_stream_pointer: BOOLEAN

is True

constant attribute

True if the underlying terminal stream has a pointer

require

is_connected

is_connected

is_connected

same_as (other: TEXT_FILE_READ): BOOLEAN

effective function

{FILE_TOOLS}

require

is_connected
other.is_connected

ensure

not is_connected
not other.is_connected

input_stream: POINTER

writable attribute

{INPUT_STREAM}

buffer: NATIVE_ARRAY[CHARACTER]

writable attribute

end_reached: BOOLEAN

writable attribute

buffer_position: INTEGER_32

writable attribute

buffer_size: INTEGER_32

writable attribute

capacity: INTEGER_32

writable attribute

fill_buffer

effective procedure

make

effective procedure

{}

The new created object is not connected.

(See also connect_to.)

ensure

not is_connected

text_file_read_open (path_pointer: POINTER): POINTER

{}

io_fclose (stream: POINTER)

{}

path: STRING

writable attribute

{ANY}

Not Void when connected to the corresponding file on the disk.

is_connected: BOOLEAN

effective function

{ANY}

Is this file connected to some file of the operating system?

ensure

definition: Result = path /= Void

set_path (new_path: ABSTRACT_STRING)

effective procedure

{}

ensure

path.same_as(new_path.out)

descriptor: INTEGER_32

effective function

{ANY}

Some OS-dependent descriptor.

Mainly used by the sequencer library (see READY_CONDITION).

require

is_connected
has_descriptor

has_descriptor: BOOLEAN

effective function

{ANY}

True if that stream can be associated to some OS-meaningful descriptor.

require

is_connected

can_disconnect: BOOLEAN

deferred function

{ANY}

True if the stream can be safely disconnected (without data loss, etc.)

require

is_connected

url: URL

frozen

effective function

{ANY}

The URL to this stream as resource

ensure

not_void: Result /= Void
always_the_same: Result = url

url_memory: URL

writable attribute

{}

new_url: URL

deferred function

{}

ensure

Result /= Void

stream_pointer: POINTER

effective function

{STREAM_HANDLER}

Some Back-end-dependent pointer (FILE* in C, InputStream or OutputStream in Java)

require

is_connected
has_stream_pointer

has_stream_pointer: BOOLEAN

effective function

{STREAM_HANDLER}

True if that stream can be associated to some Back-end-meaningful stream pointer.

require

is_connected

event_exception: EVENT_DESCRIPTOR

effective function

{ANY}

stream_exception: STREAM_EXCEPTION

writable attribute

{}

recycle

effective procedure

{RECYCLING_POOL}

Do whatever needs to be done to free resources or recycle other objects when recycling this one

dispose

effective procedure

{}

Action to be executed just before garbage collection reclaims an object.

sequencer_descriptor (file: POINTER): INTEGER_32

{}

can_read_character: BOOLEAN

is True

constant attribute

{ANY}

Note that this state is usually temporary.

Usually it is called until either it becomes True or the stream is disconnected:

 from
 until
    stream.can_read_character or else not stream.is_connected
 loop
    -- some "still waiting..." code, maybe a sandglass?
 end
 if stream.is_connected then
    stream.read_character
 end

See also: is_connected, end_of_input

require

is_connected

ensure

Result implies not end_of_input

can_read_line: BOOLEAN

is True

constant attribute

{ANY}

require

is_connected

valid_last_character: BOOLEAN

effective function

{ANY}

require

is_connected

read_character

effective procedure

{ANY}

If read_character fail, end_of_input is set.

Else, use last_character. Read tutorial or io cluster documentation to learn the read_character usage pattern.

require

is_connected
not is_filtered and then can_read_character

ensure

is_connected
not end_of_input implies valid_last_character

read_line_in (buffer: STRING)

effective procedure

{ANY}

Same job as read_line but storage is directly done in buffer.

Read tutorial or io cluster documentation to learn the read_line usage pattern.

require

is_connected
not is_filtered and then can_read_line
buffer /= Void

read_available_in (buffer: STRING, limit: INTEGER_32)

effective procedure

{ANY}

Same job as read_available but storage is directly done in buffer.

The usage pattern is the same as for read_line.

require

is_connected
not is_filtered
buffer /= Void
limit > 0

unread_character

effective procedure

{ANY}

require

is_connected
not is_filtered and then can_unread_character

ensure

not end_of_input

last_character: CHARACTER

effective function

{ANY}

require

is_connected
not end_of_input
not is_filtered and then valid_last_character

ensure

is_connected
not end_of_input

detach

effective procedure

{ANY}

Shake off the filter.

ensure

not is_filtered

filter: FILTER_INPUT_STREAM

writable attribute

The filter that uses this stream as backend

event_can_read: EVENT_DESCRIPTOR

effective function

{ANY}

can_read: CAN_READ_DATA_FROM_STREAM

writable attribute

{}

is_filtered: BOOLEAN

deferred function

{ANY}

skip_separators

effective procedure

{ANY}

Skip all separators (see is_separator of class CHARACTER) and make the first non-separator available in last_character.

This non-separator character is pushed back into the stream (see unread_character) to be available one more time (the next read_character will consider this non-separator). When end_of_input occurs, this process is automatically stopped.

require

is_connected
not is_filtered

skip_separators_using (separators: STRING)

effective procedure

{ANY}

Same job as skip_separators using the separators set.

require

is_connected
not is_filtered
separators /= Void

skip_remainder_of_line

effective procedure

{ANY}

Skip all the remainder of the line including the end of line delimiter itself.

require

is_connected
not is_filtered

read_integer

effective procedure

{ANY}

Read an integer according to the Eiffel syntax.

 Make result available in last_integer.  Heading
separators are automatically skipped using is_separator of class CHARACTER.  Trailing separators
are not skipped.

require

is_connected
not is_filtered

ensure

old end_of_input implies end_of_input and then not valid_last_integer

last_integer: INTEGER_32

writable attribute

{ANY}

Last integer read using read_integer.

valid_last_integer: BOOLEAN

writable attribute

{ANY}

Was the last call to read_integer successful ?

last_real: REAL_64

writable attribute

{ANY}

Last real read with read_real.

valid_last_real: BOOLEAN

writable attribute

{ANY}

Was the last call to read_real successful ?

read_real

effective procedure

{ANY}

Read a REAL and make the result available in last_real.

require

is_connected
not is_filtered

ensure

old end_of_input implies end_of_input and then not valid_last_real

last_string: STRING

once function

{ANY}

Access to the unique common buffer to get for example the result computed by read_line, read_word, newline, etc.

This is a once function (the same common buffer is used for all streams).

read_line

effective procedure

{ANY}