# HG changeset patch
# User wenzelm
# Date 1666371948 -7200
# Node ID 908433a347d1ecb5d6b90699a372a53b9266f171
# Parent  3698d0f3da18f910d9e286a9795653bd3d02b841
tuned signature;

diff -r 3698d0f3da18 -r 908433a347d1 src/Pure/General/url.scala
--- 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 */
diff -r 3698d0f3da18 -r 908433a347d1 src/Tools/jEdit/src/isabelle_encoding.scala
--- 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()
       }