--- a/src/Pure/General/url.scala Fri Oct 21 18:06:32 2022 +0200
+++ b/src/Pure/General/url.scala Fri Oct 21 19:05:48 2022 +0200
@@ -64,8 +64,8 @@
/* strings */
- def decode(s: String): String = URLDecoder.decode(s, UTF8.charset_name)
- def encode(s: String): String = URLEncoder.encode(s, UTF8.charset_name)
+ def decode(s: String): String = URLDecoder.decode(s, UTF8.charset)
+ def encode(s: String): String = URLEncoder.encode(s, UTF8.charset)
/* read */
--- a/src/Tools/jEdit/src/isabelle_encoding.scala Fri Oct 21 18:06:32 2022 +0200
+++ b/src/Tools/jEdit/src/isabelle_encoding.scala Fri Oct 21 19:05:48 2022 +0200
@@ -52,7 +52,7 @@
override def getTextWriter(out: OutputStream): Writer = {
val buffer = new ByteArrayOutputStream(BUFSIZE) {
override def flush(): Unit = {
- val text = Symbol.encode(toString(UTF8.charset_name))
+ val text = Symbol.encode(toString(UTF8.charset))
out.write(UTF8.bytes(text))
out.flush()
}