isabelle: src/Pure/General/utf8.scala@8585399f26f6 (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
	Fri, 05 Jul 2024 11:38:21 +0200
changeset 80508	8585399f26f6
parent 80494	d1240adc30ce
permissions	-rw-r--r--