raw symbols: allow non-ASCII chars (e.g. UTF-8);
authorwenzelm
Tue, 11 Oct 2005 13:28:07 +0200
changeset 17823 4735c07399c8
parent 17822 3830b0a41d51
child 17824 36b2978d339a
raw symbols: allow non-ASCII chars (e.g. UTF-8); tuned comment;
src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Tue Oct 11 13:28:06 2005 +0200
+++ b/src/Pure/General/symbol.ML	Tue Oct 11 13:28:07 2005 +0200
@@ -69,7 +69,7 @@
   string, may be of the following form:
 
     (1) ASCII symbols: a
-    (2) printable symbols: \<ident>
+    (2) regular symbols: \<ident>
     (3) control symbols: \<^ident>
     (4) raw control symbols: \<^raw:...>, where "..." may be any printable
         character excluding ">", or \<^raw000>
@@ -138,7 +138,8 @@
 
 (* encode_raw *)
 
-fun raw_chr c = ord space <= ord c andalso ord c <= ord "~" andalso c <> ">";
+fun raw_chr c = ord space <= ord c andalso ord c <= ord "~" andalso c <> ">"
+  orelse ord c >= 128;
 
 fun encode_raw str =
   let