# HG changeset patch
# User wenzelm
# Date 1153862261 -7200
# Node ID 7b2958d3d5754348d7bed68b7f2460f33e0e7edb
# Parent  2842450d0eee67b2b2f430b3235ba459910ce79c
raw symbols: disallow dot to avoid confusion in NameSpace.unpack;

diff -r 2842450d0eee -r 7b2958d3d575 doc-src/IsarImplementation/Thy/prelim.thy
--- a/doc-src/IsarImplementation/Thy/prelim.thy	Tue Jul 25 21:18:12 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/prelim.thy	Tue Jul 25 23:17:41 2006 +0200
@@ -47,9 +47,10 @@
 "ident"}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'',
 
 \item or a raw control symbol ``\verb,\,\verb,<^raw:,@{text
-"\<dots>"}\verb,>,'' where ``@{text "\<dots>"}'' refers to any printable ASCII
-character (excluding ``\verb,>,'') or non-ASCII character, for example
-``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
+"\<dots>"}\verb,>,'' where ``@{text "\<dots>"}'' refers to any
+printable ASCII character (excluding ``\verb,.,'' and ``\verb,>,'') or
+non-ASCII character, for example ``\verb,\,\verb,<^raw:$\sum_{i =
+1}^n$>,'',
 
 \item or a numbered raw control symbol ``\verb,\,\verb,<^raw,@{text
 "nnn"}\verb,>, where @{text "nnn"} are digits, for example
diff -r 2842450d0eee -r 7b2958d3d575 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Tue Jul 25 21:18:12 2006 +0200
+++ b/src/Pure/General/symbol.ML	Tue Jul 25 23:17:41 2006 +0200
@@ -79,7 +79,7 @@
     (2) regular symbols: \<ident>
     (3) control symbols: \<^ident>
     (4) raw control symbols: \<^raw:...>, where "..." may be any printable
-        character excluding ">", or \<^raw000>
+        character (excluding ".", ">"), or \<^raw000>
 
   Output is subject to the print_mode variable (default: verbatim),
   actual interpretation in display is up to front-end tools.
@@ -156,7 +156,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 <> "." andalso c <> ">"
   orelse ord c >= 128;
 
 fun encode_raw str =