--- a/src/Pure/General/utf8.scala Fri Oct 21 19:05:48 2022 +0200
+++ b/src/Pure/General/utf8.scala Fri Oct 21 19:08:18 2022 +0200
@@ -8,7 +8,6 @@
import java.nio.charset.Charset
-import scala.io.Codec
object UTF8 {
@@ -16,7 +15,6 @@
val charset_name: String = "UTF-8"
val charset: Charset = Charset.forName(charset_name)
- def codec(): Codec = Codec(charset)
def bytes(s: String): Array[Byte] = s.getBytes(charset)
--- a/src/Tools/jEdit/src/isabelle_encoding.scala Fri Oct 21 19:05:48 2022 +0200
+++ b/src/Tools/jEdit/src/isabelle_encoding.scala Fri Oct 21 19:08:18 2022 +0200
@@ -40,10 +40,10 @@
}
override def getTextReader(in: InputStream): Reader =
- text_reader(in, UTF8.codec(), true)
+ text_reader(in, Codec(UTF8.charset), true)
override def getPermissiveTextReader(in: InputStream): Reader = {
- val codec = UTF8.codec()
+ val codec = Codec(UTF8.charset)
codec.onMalformedInput(CodingErrorAction.REPLACE)
codec.onUnmappableCharacter(CodingErrorAction.REPLACE)
text_reader(in, codec, false)