isabelle: src/Pure/General/utf8.scala@b2b88d5b01b6 (annotated)

64639 bad5de3f9554 clarified directories; wenzelm parents: 64617 diff changeset	1	/* Title: Pure/General/utf8.scala
50203 00d8ad713e32 explicit module UTF8; wenzelm parents: diff changeset	2	Author: Makarius
00d8ad713e32 explicit module UTF8; wenzelm parents: diff changeset	3
00d8ad713e32 explicit module UTF8; wenzelm parents: diff changeset	4	Variations on UTF-8.
00d8ad713e32 explicit module UTF8; wenzelm parents: diff changeset	5	*/
00d8ad713e32 explicit module UTF8; wenzelm parents: diff changeset	6
00d8ad713e32 explicit module UTF8; wenzelm parents: diff changeset	7	package isabelle
00d8ad713e32 explicit module UTF8; wenzelm parents: diff changeset	8
00d8ad713e32 explicit module UTF8; wenzelm parents: diff changeset	9
76357 49463aef2ead tuned signature, following isabelle.setup.Environment; wenzelm parents: 76356 diff changeset	10	import java.nio.charset.{Charset, StandardCharsets}
50203 00d8ad713e32 explicit module UTF8; wenzelm parents: diff changeset	11
00d8ad713e32 explicit module UTF8; wenzelm parents: diff changeset	12
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73561 diff changeset	13	object UTF8 {
76357 49463aef2ead tuned signature, following isabelle.setup.Environment; wenzelm parents: 76356 diff changeset	14	val charset: Charset = StandardCharsets.UTF_8
50203 00d8ad713e32 explicit module UTF8; wenzelm parents: diff changeset	15
62527 aae9a2a855e0 tuned signature; wenzelm parents: 54444 diff changeset	16	def bytes(s: String): Array[Byte] = s.getBytes(charset)
50203 00d8ad713e32 explicit module UTF8; wenzelm parents: diff changeset	17	}

author	wenzelm
	Thu, 07 Aug 2025 22:42:21 +0200
changeset 82968	b2b88d5b01b6
parent 80508	8585399f26f6
permissions	-rw-r--r--