# HG changeset patch
# User paulson
# Date 1110902861 -3600
# Node ID f855fd163b62ef1ff722e960c7eeb401aa7bd2c0
# Parent  d12c459e2325ee4f53d4ccb884c8694ded62d98c
more concise ASCII escaping

diff -r d12c459e2325 -r f855fd163b62 src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Mon Mar 14 20:30:43 2005 +0100
+++ b/src/HOL/Tools/res_clause.ML	Tue Mar 15 17:07:41 2005 +0100
@@ -79,15 +79,28 @@
 
 
 
+(*Escaping of special characters.
+  Alphanumeric characters are left unchanged.
+  The character _ goes to __
+  Characters in the range ASCII space to / go to _A to _P, respectively.
+  Other printing characters go to _NNN where NNN is the decimal ASCII code.*)
+local
+
+val A_minus_space = Char.ord #"A" - Char.ord #" ";
+
 fun ascii_of_c c =
-    let val n = ord c
-    in
-	(if ((n < 48) orelse (n > 57 andalso n < 65) orelse 
-	   (n > 90 andalso n < 97) orelse (n > 122)) then ("_asc" ^ string_of_int n ^ "_")
-							 else c)
-    end;
+  if Char.isAlphaNum c then String.str c
+  else if c = #"_" then "__"
+  else if #" " <= c andalso c <= #"/" 
+       then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space))
+  else if Char.isPrint c then ("_" ^ Int.toString (Char.ord c))
+  else ""
 
-fun ascii_of s = implode(map ascii_of_c (explode s));
+in
+
+val ascii_of = String.translate ascii_of_c;
+
+end;
 
 
 (* another version of above functions that remove chars that may not be allowed by Vampire *)