9 Sep
2008
9 Sep
'08
12:35 p.m.
Makarius wrote:
I am working with named pipes to output large amounts of text to an external process. Looking at the sources of basis/TextIO.sml etc. I've got the impression that pipes are always line-buffered. Is there an easy way to get block-buffering?
Currently TextIO.openOut sets line buffering for terminals, pipes and devices. Looking at the Basis Library document it seems that the stream should be block buffered unless it's a terminal so I'll change this.
In the meantime you can of course use TextIO.StreamIO.setBufferMode(TextIO.getOutstream f, IO.BLOCK_BUF);
David