# 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() }