added string_bytes convenience;
authorwenzelm
Tue Aug 10 18:24:16 2010 +0200 (2010-08-10)
changeset 38264205b74a1bb18
parent 38263 11c2b8d1fde0
child 38265 cc9fde54311f
added string_bytes convenience;
src/Pure/System/standard_system.scala
     1.1 --- a/src/Pure/System/standard_system.scala	Tue Aug 10 18:23:12 2010 +0200
     1.2 +++ b/src/Pure/System/standard_system.scala	Tue Aug 10 18:24:16 2010 +0200
     1.3 @@ -19,9 +19,13 @@
     1.4  
     1.5  object Standard_System
     1.6  {
     1.7 +  /* UTF-8 charset */
     1.8 +
     1.9    val charset = "UTF-8"
    1.10    def codec(): Codec = Codec(charset)
    1.11  
    1.12 +  def string_bytes(s: String): Array[Byte] = s.getBytes(charset)
    1.13 +
    1.14  
    1.15    /* permissive UTF-8 decoding */
    1.16