deferred class FILTER

All features

A filter is something connected to a stream. It allows to add behaviour (e.g. compression, encryption and any other codings)

There are two kinds of filters: + input filters (see FILTER_INPUT_STREAM) + output filters (see FILTER_OUTPUT_STREAM)

Direct parents

non-conformant parents

ANY

Known children

conformant children

FILTER_INPUT_STREAM, FILTER_OUTPUT_STREAM

Summary

exported features

Details

connect_to (a_stream: STREAM)

Connect the filter to some underlying stream.

require

  • not is_connected
  • a_stream.is_connected
  • not a_stream.is_filtered

ensure

  • is_connected

is_connected: BOOLEAN

True if the filter is connected to some underlying stream.

deferred disconnect

Disconnect from the underlying stream.

require

  • is_connected
  • can_disconnect

ensure

  • not is_connected
  • stream = Void

can_disconnect: BOOLEAN
filtered_descriptor: INTEGER
filtered_has_descriptor: BOOLEAN
filtered_stream_pointer: POINTER
filtered_has_stream_pointer: BOOLEAN
deferred local_can_disconnect: BOOLEAN

True if this stream can be safely disconnected (without data loss, etc.) without taking into account the state of the underlying stream.

stream: STREAM

The underlying stream (i.e. the filtered one)

deferred do_detach

Used by the underlying stream to require not to be filtered anymore

Class invariant