[m-rev.] diff: workaround an issue causing test failures in the C# grades

[Julien Fischer]

The proper fix for this would be to redo how file streams are handled
in Mercury,
as per some of the existing XXX comments.  In particular, while having
io.stream works
for the C backends where the underlying file representation is the
same for all the
different Mercury stream types, it doesn't work for the Java and C#
backends where
we really want to have different target language types for each
Mercury stream type.

-----------------------------------

Workaround an issue causing test failures in the C# grade.

A number of test cases are currently failing in the C# grade due to
ObjectDisposedExceptions being thrown when a binary output file is closed.
This is being caused by the way Mercury files are currently
implemented in C#.  In
particular, Mercury output streams have both a TextWriter and a BufferredStream
attached to the same underlying IO stream. The C# implementation of
stream_ops.close_stream/4 works by closing the TextWriter and then closing the
BufferedStream. Closing the TextWriter also closes the IO stream, which triggers
the exception when then closing the BufferedStream _unless_ the buffer is empty.
The workaround is to flush the BufferedStream before we close the TextWriter.
(I think something must have changed in, at least, Mono since this was working
previously).

library/io.stream_ops.m:
    Flush the BufferedStream stored in the C# version of a Mercury file before
    closing the TextWriter.

    Add some XXX comments about this and about the way binary streams are
    handled.

Julien.

diff --git a/library/io.stream_ops.m b/library/io.stream_ops.m
index b467763c7..ace2abc17 100644
--- a/library/io.stream_ops.m
+++ b/library/io.stream_ops.m
@@ -1731,9 +1731,13 @@ public class MR_MercuryFileStruct {
     // so exactly one of the following two fields will used (and be non-null)
     // for any particular stream.
     // Note also that we use the TextReader class interface to read both
-    // text AND binary files, and like use the TextWriter class interface
+    // text AND binary files, and likewise the TextWriter class interface
     // to write both text and binary files, which to me (zs) looks strange,
     // given that C# also has a System.IO.BinaryReader class.
+    // XXX The bit about using TextReaders and TextWriters to read and write
+    // binary streams is not true. We actually wrap a BufferedStream (which is
+    // what the stream field here is) around the underlying IO.Stream and use
+    // that for binary file operations.
     //
     // XXX Using four subclasses, for text input, binary input,
     // text output and binary output, as the Java code above does,
@@ -1845,6 +1849,11 @@ mercury_close(MR_MercuryFileStruct mf)
         mf.reader = null;
     }
     if (mf.writer != null) {
+        // XXX The call to Flush() here is a workaround for the fact that call
+        // to mf.writer.Close() will dispose of the underlying IO stream and
+        // this will cause the call to mf.stream.Close() below to throw an
+        // an exception *unless* the buffer is empty.
+        mf.stream.Flush();
         mf.writer.Close();
         mf.writer = null;
     }