added string_bytes convenience;
authorwenzelm
Tue, 10 Aug 2010 18:24:16 +0200
changeset 38264 205b74a1bb18
parent 38263 11c2b8d1fde0
child 38265 cc9fde54311f
added string_bytes convenience;
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 */