--- 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,
--- 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)
--- 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