unused;
authorwenzelm
Fri May 11 19:59:05 2018 +0200 (12 months ago)
changeset 681499a4a6adb95b5
parent 68148 fb661e4c4717
child 68150 f0f34cbed539
unused;
src/Pure/General/bytes.scala
src/Pure/library.ML
     1.1 --- a/src/Pure/General/bytes.scala	Fri May 11 19:57:49 2018 +0200
     1.2 +++ b/src/Pure/General/bytes.scala	Fri May 11 19:59:05 2018 +0200
     1.3 @@ -40,22 +40,6 @@
     1.4      }
     1.5  
     1.6  
     1.7 -  def hex(s: String): Bytes =
     1.8 -  {
     1.9 -    def err(): Nothing = error("Malformed hexadecimal representation of bytes\n" + s)
    1.10 -    val len = s.length
    1.11 -    if (len % 2 != 0) err()
    1.12 -
    1.13 -    val n = len / 2
    1.14 -    val a = new Array[Byte](n)
    1.15 -    for (i <- 0 until n) {
    1.16 -      val j = 2 * i
    1.17 -      try { a(i) = Integer.parseInt(s.substring(j, j + 2), 16).toByte }
    1.18 -      catch { case _: NumberFormatException => err() }
    1.19 -    }
    1.20 -    new Bytes(a, 0, n)
    1.21 -  }
    1.22 -
    1.23    def base64(s: String): Bytes =
    1.24    {
    1.25      val a = Base64.getDecoder.decode(s)
     2.1 --- a/src/Pure/library.ML	Fri May 11 19:57:49 2018 +0200
     2.2 +++ b/src/Pure/library.ML	Fri May 11 19:59:05 2018 +0200
     2.3 @@ -155,7 +155,6 @@
     2.4    val translate_string: (string -> string) -> string -> string
     2.5    val encode_lines: string -> string
     2.6    val decode_lines: string -> string
     2.7 -  val hex_string: string -> string
     2.8    val align_right: string -> int -> string -> string
     2.9    val match_string: string -> string -> bool
    2.10  
    2.11 @@ -777,12 +776,6 @@
    2.12  val encode_lines = translate_string (fn "\n" => "\v" | c => c);
    2.13  val decode_lines = translate_string (fn "\v" => "\n" | c => c);
    2.14  
    2.15 -fun hex_string s =
    2.16 -  fold_string (fn c =>
    2.17 -    let val (a, b) = IntInf.divMod (ord c, 16)
    2.18 -    in cons (hex_digit a) #> cons (hex_digit b) end) s []
    2.19 -  |> rev |> implode;
    2.20 -
    2.21  fun align_right c k s =
    2.22    let
    2.23      val _ = if size c <> 1 orelse size s > k