[m-dev.] a chunk type?

[Peter Wang]

Hi,

Does anyone have any objection to adding a string.chunk type, analogous
to the string.line and string.text_file types?  The intention is to be
able to use stream.get to read some arbitrary number of characters out
of a stream.  The number could be just something convenient for the
stream, or some stream types could provide predicates to record the
desired chunk size.

Better ideas?

Peter

--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at csse.unimelb.edu.au
Administrative Queries: owner-mercury-developers at csse.unimelb.edu.au
Subscriptions:          mercury-developers-request at csse.unimelb.edu.au
--------------------------------------------------------------------------