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.
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
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 <rda at lemma-one.com> wrote:
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
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 associate the reader or writer with a different stream. Here you have to reassociate the reader or writer with the original stream to get it working again.
Regards,
Rob.
On 7 May 2016, at 11:56, Rob Arthan <rda at lemma-one.com> wrote:
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
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
-
Michael.Norrish＠nicta.com.au -
rda＠lemma-one.com