--- 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
--- 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 =