+
Point of view
All features
class SPLIT_OUTPUT_STREAM
- line_length > 0
- stream /= Void implies stream.filter = Current
Default_line_separator:
STRING
constant attribute
require
- not is_connected
- a_stream.is_connected
- not a_stream.is_filtered
ensure
set_line_separator (a_separator:
STRING)
effective procedure
require
- is_connected
- can_put_character(c)
require
- is_connected
- can_disconnect
- is_connected
- can_disconnect
- is_connected
- can_disconnect
ensure
- not is_connected
- stream = Void
- not is_filtered
require
- is_connected
- not is_filtered and then can_put_character(c)
filtered_has_stream_pointer:
BOOLEAN
deferred function
frozen
effective procedure
frozen
effective procedure
append_file (file_name:
STRING)
effective procedure