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) = TextIO.StreamIO.getWriter(TextIO.getOutstream outstream); val _ = TextIO.setOutstream (outstream, TextIO.StreamIO.mkOutstream(wr, buf)); in case ioDesc of NONE => false | SOME desc => (OS.IO.kind desc = OS.IO.Kind.tty) end );
For reasons that I don?t claim to understand, the stream behaves as if it is closed after the call to getWriter. You have to use setOutstream (or setInstream in is_term_in) to fix that before anything (e.g., the read-eval-print loop) attempts to do I/O on the stream.
Regards,
Rob.
On 7 May 2016, at 06:01, Michael Norrish <Michael.Norrish at nicta.com.au> wrote:
The Basis library documentation for OS.IO suggests that it should be possible to get one's hand on a primitive reader or writer iodesc by pulling things apart to get PrimIO values.
Doing type-directed programming, I thought I might do this for a TextIO.outstream with
val getIOD = (fn TextPrimIO.WR r => #ioDesc r) o #1 o TextIO.StreamIO.getWriter o TextIO.getOutstream;
val getIOD = fn: TextIO.outstream -> OS.IO.iodesc option
This has the right type (and I couldn't see any other way of getting the right type). Unfortunately, I can't run it:
getIOD TextIO.stdOut;
Exception Io raised while writing to stdOut.
terminating the session.
If this had worked, I then hoped to be able to call Posix.FileSys.iodToFD on the value, if there was one, and to then eventually call Posix.ProcEnv.isatty on the result of that, if present.
Is there a right way to do this?
Many thanks, Michael
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. _______________________________________________ polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml