# HG changeset patch
# User wenzelm
# Date 1666372098 -7200
# Node ID 16816ee9a570ac72f68fc72423669db4f6a01cca
# Parent  908433a347d1ecb5d6b90699a372a53b9266f171
tuned signature;

diff -r 908433a347d1 -r 16816ee9a570 src/Pure/General/utf8.scala
--- 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)
 
diff -r 908433a347d1 -r 16816ee9a570 src/Tools/jEdit/src/isabelle_encoding.scala
--- 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)