home
wiki
classes/clusters list
class information
+
Point of view
All features
ANY
STREAM
FILTER
INTERNALS_HANDLER
All features
deferred class FILTER
Summary
top
A filter is something connected to a stream. It allows to add behavior (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
insert list:
ANY
Known children
insert list:
FILTER_INPUT_STREAM
,
FILTER_OUTPUT_STREAM
Class invariant
top
stream
/= Void implies
stream
.filter = Current
Overview
top
features
connect_to
(a_stream:
FILTERABLE
)
Connect the filter to some underlying stream.
is_connected
:
BOOLEAN
True if the filter is connected to some underlying stream.
disconnect
Disconnect from the underlying stream.
can_disconnect
:
BOOLEAN
filtered_descriptor
:
INTEGER_32
filtered_has_descriptor
:
BOOLEAN
filtered_stream_pointer
:
POINTER
filtered_has_stream_pointer
:
BOOLEAN
local_can_disconnect
:
BOOLEAN
True if this stream can be safely disconnected (without data loss, etc.)
stream
:
FILTERABLE
The underlying stream (i.e. the filtered one)
do_detach
Used by the underlying stream to require not to be filtered anymore
connect_to
(a_stream:
FILTERABLE
)
effective procedure
top
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
effective function
top
True if the filter is connected to some underlying stream.
disconnect
deferred procedure
top
Disconnect from the underlying stream.
require
is_connected
can_disconnect
ensure
not
is_connected
stream
= Void
can_disconnect
:
BOOLEAN
effective function
top
filtered_descriptor
:
INTEGER_32
effective function
top
filtered_has_descriptor
:
BOOLEAN
effective function
top
filtered_stream_pointer
:
POINTER
effective function
top
filtered_has_stream_pointer
:
BOOLEAN
effective function
top
local_can_disconnect
:
BOOLEAN
deferred function
top
True if this stream can be safely disconnected (without data loss, etc.)
without taking into account the state of the underlying stream.
stream
:
FILTERABLE
writable attribute
top
The underlying stream (i.e. the filtered one)
do_detach
deferred procedure
top
Used by the underlying stream to require not to be filtered anymore
ensure
stream
= Void