#253 Option to choose default file encoding
This request arose from the following email:
****************
From: micchii_jp@hotmail.com
Subject: [JAVAPLT] question
Date: May 15, 2005 1:32:45 AM CDT
To: javaplt@rice.edu
Helo. I have a question with DrJava.
When I type japanese or chinese on DrJava, it displays them
correctly. But when I open the file after I saved and closed, it can't
display. Those characters are all "?".
Can't we make java programs with DrJava using foreign languages?
Please tell me.
Thank you.
****************
I would suggest adding a drop-down list to the preferences dialog box
that lists all the platform's supported character encodings
(java.nio.charset.Charset.availableCharsets()) and lets the user
choose one for all document reading and writing. The actual
encoding change could be implemented (I believe) by invoking
DefaultEditorKit.write(Writer, Document, int, int) instead of
DefaultEditorKit.write(OutputStream, Document, int, int), providing an
appropriately-configured Writer.
