author | wenzelm |
Tue, 10 Aug 2010 18:24:16 +0200 | |
changeset 38264 | 205b74a1bb18 |
parent 38263 | 11c2b8d1fde0 |
child 38265 | cc9fde54311f |
--- a/src/Pure/System/standard_system.scala Tue Aug 10 18:23:12 2010 +0200 +++ b/src/Pure/System/standard_system.scala Tue Aug 10 18:24:16 2010 +0200 @@ -19,9 +19,13 @@ object Standard_System { + /* UTF-8 charset */ + val charset = "UTF-8" def codec(): Codec = Codec(charset) + def string_bytes(s: String): Array[Byte] = s.getBytes(charset) + /* permissive UTF-8 decoding */