# HG changeset patch
# User wenzelm
# Date 1457261975 -3600
# Node ID aae9a2a855e0a9deeaead6892240a438286c421d
# Parent  347150095fd25aabab32df27ec33c0f2027db222
tuned signature;

diff -r 347150095fd2 -r aae9a2a855e0 src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Sun Mar 06 10:33:34 2016 +0100
+++ b/src/Pure/General/bytes.scala	Sun Mar 06 11:59:35 2016 +0100
@@ -20,7 +20,7 @@
     val str = s.toString
     if (str.isEmpty) empty
     else {
-      val b = str.getBytes(UTF8.charset)
+      val b = UTF8.bytes(str)
       new Bytes(b, 0, b.length)
     }
   }
diff -r 347150095fd2 -r aae9a2a855e0 src/Pure/System/utf8.scala
--- a/src/Pure/System/utf8.scala	Sun Mar 06 10:33:34 2016 +0100
+++ b/src/Pure/System/utf8.scala	Sun Mar 06 11:59:35 2016 +0100
@@ -20,6 +20,8 @@
   val charset: Charset = Charset.forName(charset_name)
   def codec(): Codec = Codec(charset)
 
+  def bytes(s: String): Array[Byte] = s.getBytes(charset)
+
 
   /* permissive UTF-8 decoding */
 
diff -r 347150095fd2 -r aae9a2a855e0 src/Tools/jEdit/src/isabelle_encoding.scala
--- a/src/Tools/jEdit/src/isabelle_encoding.scala	Sun Mar 06 10:33:34 2016 +0100
+++ b/src/Tools/jEdit/src/isabelle_encoding.scala	Sun Mar 06 11:59:35 2016 +0100
@@ -56,7 +56,7 @@
       override def flush()
       {
         val text = Symbol.encode(toString(UTF8.charset_name))
-        out.write(text.getBytes(UTF8.charset))
+        out.write(UTF8.bytes(text))
         out.flush()
       }
       override def close() { out.close() }