Re: [polyml] determining if an outstream is a tty

2016-05-07 Thread Rob Arthan
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

Re: [polyml] determining if an outstream is a tty

2016-05-07 Thread Michael Norrish
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

Re: [polyml] determining if an outstream is a tty

2016-05-07 Thread Rob Arthan
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) =