Section "stream"

The stream API provides access to the objects representing text input/output streams. This is to allow custom implementations beyond the standard. The input reader transparently handles ‘\n’, ‘\r\n’ and ‘\r’ as newline whereby also counting line numbers. The output writer does buffer before flushing and keeps track of the last written character.

Th input call-back is a function that takes no argument and returns a string. Returning an emp-ty string indicates that end-of-stream has been reached. The output call-back is a function that takes a string and that doesn’t return anything. In both cases, to cater for call-backs that de-pend on some stream, appropriate host closures need to be created.

The following term API calls are provided:

new Source(T, R, C, D): (host language)
Create a text input with initial text T, call-back R, call-back C and data D.
new Sink(S, N, C, D): (host language)
Create a text output with call-back S, call-back N, call-back C and data D.
check_source(T): (host language)
Assure that the object T is a text input.
check_sink(T): (host language)
Assure that the object T is a text output.

Kommentare