7.6.2 Reading from Streams

Unlike normal Unix file descriptors, read-only poke streams are buffered. Let’s supposed we open the standard input:

var stdin = open ("<stdin>");

Then we map some data (one byte) at some particular offset:

var b = byte @ stdin : 28#B;

The mapping operation above causes poke to read 28 bytes from the standard input and to set the variable b to the 28-th byte. The bytes read from the stream are still available (buffered) and the offsets are still relative from the “beginning” of the standard input:

var c = byte @stdin : 0#B;

The byte in c is the byte that appeared in the standard input 27 bytes before the byte in b.

This buffering is nice, and it is what allows us to access the standard input like if it were a random oriented device. However, it is obvious we would be in trouble if we filter big amounts of data, like in a network interface: we would likely use all available memory.

To allow filtering big amount of data, poke allows to flush the read-only streams. Flushing means that the buffered data in the read-only stream is “forgotten”, and trying to access it will result in an exception:

var stdin = open ("<stdin>");

var b = byte @ stdin : 28#B;
var c = byte @ stdin : 29#B;
flush (stdin, 29#B);
var d = byte @ stdin : 30#B;
var e = byte @ stdin : 20#B; /* Exception.  */