# HG changeset patch
# User wenzelm
# Date 1277413125 -7200
# Node ID 62eb9d03b221e1b60abcb9665c99b26ab2933ada
# Parent  d775bd70f571b6eef4cd600e360f8d88fbd71c6b
escape UTF8 symbols for the ML compiler;

diff -r d775bd70f571 -r 62eb9d03b221 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Thu Jun 24 21:57:18 2010 +0200
+++ b/src/Pure/General/symbol.ML	Thu Jun 24 22:58:45 2010 +0200
@@ -491,7 +491,11 @@
 
 (* escape *)
 
-val esc = fn s => if is_char s then s else "\\" ^ s;
+val esc = fn s =>
+  if is_char s then s
+  else if is_utf8 s then translate_string (fn c => "\\" ^ string_of_int (ord c)) s
+  else "\\" ^ s;
+
 val escape = implode o map esc o sym_explode;