deferred class STREAM

Features exported to STREAM_HANDLER

A stream of characters.

There are two kinds of streams: + input streams (see INPUT_STREAM) + output_streams (see OUTPUT_STREAM)

Streams can: + be connected (e.g. to some system object) + be used ot read or write characters, only if they are connected + be filtered (see FILTER)

Direct parents

non-conformant parents

ANY

Known children

conformant children

INPUT_STREAM

non-conformant children

OUTPUT_STREAM

Summary

exported features

Details

deferred is_connected: BOOLEAN

True if the stream is connected. Only in that case can data be transfered via this stream.

deferred disconnect

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

ensure

  • not is_filtered

is_filtered: BOOLEAN

True if some filter is using this stream as backend. use that filter instead.

deferred detach

Shake off the filter.

ensure

  • not is_filtered

descriptor: INTEGER

Some OS-dependent descriptor. Mainly used by the sequencer library (see READY_CONDITION).

require

  • is_connected
  • has_descriptor

has_descriptor: BOOLEAN

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

require

  • is_connected

deferred can_disconnect: BOOLEAN

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

require

  • is_connected

stream_pointer: POINTER

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

require

  • is_connected
  • has_stream_pointer

has_stream_pointer: BOOLEAN

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

require

  • is_connected