--- a/src/Tools/jEdit/dist-template/properties/jedit.props Thu Jun 25 21:15:28 2009 +0200
+++ b/src/Tools/jEdit/dist-template/properties/jedit.props Thu Jun 25 23:03:09 2009 +0200
@@ -1,12 +1,12 @@
#jEdit properties
buffer.deepIndent=false
-buffer.encoding=UTF-8
+buffer.encoding=UTF-8-isabelle
buffer.indentSize=2
buffer.lineSeparator=\n
buffer.maxLineLen=100
buffer.noTabs=true
buffer.tabSize=2
-fallbackEncodings=US-ASCII ISO-8859-15
+fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII
firstTime=false
tip.show=false
encodingDetectors=BOM XML-PI buffer-local-property
--- a/src/Tools/jEdit/plugin/services.xml Thu Jun 25 21:15:28 2009 +0200
+++ b/src/Tools/jEdit/plugin/services.xml Thu Jun 25 23:03:09 2009 +0200
@@ -1,12 +1,15 @@
<?xml version="1.0"?>
<!DOCTYPE SERVICES SYSTEM "services.dtd">
<SERVICES>
+ <SERVICE NAME="isabelle" CLASS="org.gjt.sp.jedit.io.VFS">
+ new isabelle.jedit.VFS();
+ </SERVICE>
+ <SERVICE NAME="UTF-8-isabelle" CLASS="org.gjt.sp.jedit.io.Encoding">
+ new isabelle.jedit.IsabelleEncoding();
+ </SERVICE>
<SERVICE NAME="isabelle" CLASS="sidekick.SideKickParser">
new isabelle.jedit.IsabelleSideKickParser();
</SERVICE>
- <SERVICE NAME="isabelle" CLASS="org.gjt.sp.jedit.io.VFS">
- new isabelle.jedit.VFS();
- </SERVICE>
<SERVICE NAME="isabelle" CLASS="gatchan.jedit.hyperlinks.HyperlinkSource">
new isabelle.jedit.IsabelleHyperlinkSource();
</SERVICE>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/IsabelleEncoding.scala Thu Jun 25 23:03:09 2009 +0200
@@ -0,0 +1,32 @@
+/*
+ * Isabelle encoding -- based on utf-8
+ *
+ * @author Makarius
+ */
+
+package isabelle.jedit
+
+import org.gjt.sp.jedit.io.Encoding
+
+import java.nio.charset.{Charset, CodingErrorAction}
+import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter}
+
+
+class IsabelleEncoding extends Encoding
+{
+ private val charset = Charset.forName(Isabelle_System.charset)
+
+ override def getTextReader(in: InputStream): Reader =
+ new InputStreamReader(in, charset.newDecoder())
+
+ override def getTextWriter(out: OutputStream): Writer =
+ new OutputStreamWriter(out, charset.newEncoder())
+
+ override def getPermissiveTextReader(in: InputStream): Reader =
+ {
+ val decoder = charset.newDecoder()
+ decoder.onMalformedInput(CodingErrorAction.REPLACE)
+ decoder.onUnmappableCharacter(CodingErrorAction.REPLACE)
+ new InputStreamReader(in, decoder)
+ }
+}