diff -r fb661e4c4717 -r 9a4a6adb95b5 src/Pure/General/bytes.scala --- a/src/Pure/General/bytes.scala Fri May 11 19:57:49 2018 +0200 +++ b/src/Pure/General/bytes.scala Fri May 11 19:59:05 2018 +0200 @@ -40,22 +40,6 @@ } - def hex(s: String): Bytes = - { - def err(): Nothing = error("Malformed hexadecimal representation of bytes\n" + s) - val len = s.length - if (len % 2 != 0) err() - - val n = len / 2 - val a = new Array[Byte](n) - for (i <- 0 until n) { - val j = 2 * i - try { a(i) = Integer.parseInt(s.substring(j, j + 2), 16).toByte } - catch { case _: NumberFormatException => err() } - } - new Bytes(a, 0, n) - } - def base64(s: String): Bytes = { val a = Base64.getDecoder.decode(s)