equal
deleted
inserted
replaced
5 */ |
5 */ |
6 |
6 |
7 package isabelle |
7 package isabelle |
8 |
8 |
9 |
9 |
10 import java.nio.charset.Charset |
10 import java.nio.charset.{Charset, StandardCharsets} |
11 |
11 |
12 |
12 |
13 object UTF8 { |
13 object UTF8 { |
14 /* charset */ |
14 /* charset */ |
15 |
15 |
16 val charset: Charset = Charset.forName("UTF-8") |
16 val charset: Charset = StandardCharsets.UTF_8 |
17 |
17 |
18 def bytes(s: String): Array[Byte] = s.getBytes(charset) |
18 def bytes(s: String): Array[Byte] = s.getBytes(charset) |
19 |
19 |
20 |
20 |
21 /* permissive UTF-8 decoding */ |
21 /* permissive UTF-8 decoding */ |