# HG changeset patch # User wenzelm # Date 1281457456 -7200 # Node ID 205b74a1bb182feeb55d8c65276fc6ce201a5a81 # Parent 11c2b8d1fde04b61099b35a059787f976931f47d added string_bytes convenience; diff -r 11c2b8d1fde0 -r 205b74a1bb18 src/Pure/System/standard_system.scala --- 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 */