# HG changeset patch
# User wenzelm
# Date 1666372238 -7200
# Node ID 92e9fa289056ef3fe4fe9ea225d9732467f71952
# Parent  16816ee9a570ac72f68fc72423669db4f6a01cca
tuned signature;

diff -r 16816ee9a570 -r 92e9fa289056 src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Fri Oct 21 19:08:18 2022 +0200
+++ b/src/Pure/General/http.scala	Fri Oct 21 19:10:38 2022 +0200
@@ -22,7 +22,7 @@
     val mime_type_html: String = "text/html; charset=utf-8"
 
     val default_mime_type: String = mime_type_bytes
-    val default_encoding: String = UTF8.charset_name
+    val default_encoding: String = UTF8.charset.name
 
     def apply(
         bytes: Bytes,
diff -r 16816ee9a570 -r 92e9fa289056 src/Pure/General/utf8.scala
--- a/src/Pure/General/utf8.scala	Fri Oct 21 19:08:18 2022 +0200
+++ b/src/Pure/General/utf8.scala	Fri Oct 21 19:10:38 2022 +0200
@@ -13,8 +13,7 @@
 object UTF8 {
   /* charset */
 
-  val charset_name: String = "UTF-8"
-  val charset: Charset = Charset.forName(charset_name)
+  val charset: Charset = Charset.forName("UTF-8")
 
   def bytes(s: String): Array[Byte] = s.getBytes(charset)
 
diff -r 16816ee9a570 -r 92e9fa289056 src/Pure/System/isabelle_charset.scala
--- a/src/Pure/System/isabelle_charset.scala	Fri Oct 21 19:08:18 2022 +0200
+++ b/src/Pure/System/isabelle_charset.scala	Fri Oct 21 19:10:38 2022 +0200
@@ -22,7 +22,7 @@
 
 class Isabelle_Charset extends Charset(Isabelle_Charset.name, null) {
   override def contains(cs: Charset): Boolean =
-    cs.name.equalsIgnoreCase(UTF8.charset_name) || UTF8.charset.contains(cs)
+    cs.name.equalsIgnoreCase(UTF8.charset.name) || UTF8.charset.contains(cs)
 
   override def newDecoder(): CharsetDecoder = UTF8.charset.newDecoder