# HG changeset patch
# User wenzelm
# Date 1343758170 -7200
# Node ID 4dd1d45859029077b4486be6bcf6bf3f14460e26
# Parent  3ef76d545aafba4f19773dc7be51cf6661dc6afd
more portable hex_nibble: avoid disagreement of Poly/ML and SML/NJ on StringCvt.HEX;

diff -r 3ef76d545aaf -r 4dd1d4585902 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Tue Jul 31 19:55:04 2012 +0200
+++ b/src/Pure/Thy/latex.ML	Tue Jul 31 20:09:30 2012 +0200
@@ -33,8 +33,11 @@
 (* literal text *)
 
 local
-  val hex = Int.fmt StringCvt.HEX;
-  fun hex_byte c = hex (ord c div 16) ^ hex (ord c mod 16);
+  fun hex_nibble i =
+    if i < 10 then string_of_int i
+    else chr (ord "A" + i - 10);
+
+  fun hex_byte c = hex_nibble (ord c div 16) ^ hex_nibble (ord c mod 16);
 in
 
 fun literal txt = "\\isaliteral{" ^ translate_string hex_byte txt ^ "}";