PS:
In fairness to the Standard ML Basis library, the behaviour is documented
and does make sense. The description of getReader and getWriter say that they
flush the stream and mark it as terminated, which is what you’d probably
want if you were going to use setInstream or setOutstream to
Thanks for this!
The documentation does say that getWriter will do this (though I don't
understand it either). I didn't think of explicitly repairing the stream.
Best wishes,
Michael
> On 7 May 2016, at 20:56, Rob Arthan wrote:
>
> Michael,
>
> I adapted this from an
Michael,
I adapted this from an analogous function is_term_in that we have in ProofPower
and it seems to work.
fun is_term_out (outstream : TextIO.outstream) = (
let val (wr as TextPrimIO.WR{ioDesc,...},buf) =