A Unicode editor for Michael

Michael claims that he does not have an editor that can handle Unicode.

Thus, Henning and I whipped up an editor using mGTK that can handle Unicode. Oh, and did I mention that you can it compile with either Moscow ML or MLton without changing the source?

The real story is of course that I we were trying to build a “real” application using mGTK, and the editor example shows that the gtk+ widgets handle Unicode fine. Wereas I’m not sure that SML handles Unicode “fine”, String.size does not return the number of characters but the number of bytes. But at least TextIO does not mess up the bytes (in Moscow ML at least, didn’t test with MLton).

Oh, and I used file and gedit to check that the file I saved really was Unicode.