# HG changeset patch
# User wenzelm
# Date 1525549458 -7200
# Node ID dac267cd51fe3dd9fdab2c63da4f16927a53303e
# Parent  9e1c670301b82f7fcaccc278538f10493a3a16de
hexadecimal representation of byte string;

diff -r 9e1c670301b8 -r dac267cd51fe src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Sat May 05 13:56:51 2018 +0200
+++ b/src/Pure/General/bytes.scala	Sat May 05 21:44:18 2018 +0200
@@ -39,6 +39,23 @@
     }
 
 
+  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)
+  }
+
+
   /* read */
 
   def read_stream(stream: InputStream, limit: Int = Integer.MAX_VALUE, hint: Int = 1024): Bytes =
diff -r 9e1c670301b8 -r dac267cd51fe src/Pure/General/sha1.ML
--- a/src/Pure/General/sha1.ML	Sat May 05 13:56:51 2018 +0200
+++ b/src/Pure/General/sha1.ML	Sat May 05 21:44:18 2018 +0200
@@ -159,7 +159,6 @@
 
 (* digesting *)
 
-fun hex_digit i = if i < 10 then chr (Char.ord #"0" + i) else chr (Char.ord #"a" + i - 10);
 fun hex_string byte = op ^ (apply2 hex_digit (Integer.div_mod (Word8.toInt byte) 16));
 
 in
diff -r 9e1c670301b8 -r dac267cd51fe src/Pure/library.ML
--- a/src/Pure/library.ML	Sat May 05 13:56:51 2018 +0200
+++ b/src/Pure/library.ML	Sat May 05 21:44:18 2018 +0200
@@ -116,6 +116,7 @@
   (*integers*)
   val upto: int * int -> int list
   val downto: int * int -> int list
+  val hex_digit: int -> string
   val radixpand: int * int -> int list
   val radixstring: int * string * int -> string
   val string_of_int: int -> string
@@ -154,6 +155,7 @@
   val translate_string: (string -> string) -> string -> string
   val encode_lines: string -> string
   val decode_lines: string -> string
+  val hex_string: string -> string
   val align_right: string -> int -> string -> string
   val match_string: string -> string -> bool
 
@@ -613,6 +615,10 @@
 
 (* convert integers to strings *)
 
+(*hexadecimal*)
+fun hex_digit i =
+  if i < 10 then chr (Char.ord #"0" + i) else chr (Char.ord #"a" + i - 10);
+
 (*expand the number in the given base;
   example: radixpand (2, 8) gives [1, 0, 0, 0]*)
 fun radixpand (base, num) : int list =
@@ -771,6 +777,12 @@
 val encode_lines = translate_string (fn "\n" => "\v" | c => c);
 val decode_lines = translate_string (fn "\v" => "\n" | c => c);
 
+fun hex_string s =
+  fold_string (fn c =>
+    let val (a, b) = IntInf.divMod (ord c, 16)
+    in cons (hex_digit a) #> cons (hex_digit b) end) s []
+  |> rev |> implode;
+
 fun align_right c k s =
   let
     val _ = if size c <> 1 orelse size s > k