# HG changeset patch
# User wenzelm
# Date 1129030087 -7200
# Node ID 4735c07399c88cb1a92443c77053e0d7a2749346
# Parent  3830b0a41d51aec6a7ac5ba536599b27b4c15b69
raw symbols: allow non-ASCII chars (e.g. UTF-8);
tuned comment;

diff -r 3830b0a41d51 -r 4735c07399c8 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