--- a/doc-src/IsarRef/syntax.tex Wed Jun 07 14:19:10 2000 +0200
+++ b/doc-src/IsarRef/syntax.tex Wed Jun 07 14:19:48 2000 +0200
@@ -65,9 +65,9 @@
The syntax of \texttt{string} admits any characters, including newlines;
``\verb|"|'' (double-quote) and ``\verb|\|'' (backslash) have to be escaped by
-a backslash. Note that ML-style control characters are \emph{not} supported.
-The body of \texttt{verbatim} may consist of any text not containing
-``\verb|*}|''.
+a backslash; newlines need not be escaped. Note that ML-style control
+characters are \emph{not} supported. The body of \texttt{verbatim} may
+consist of any text not containing ``\verb|*}|''.
Comments take the form \texttt{(*~\dots~*)} and may be
nested\footnote{Proof~General may occasionally get confused by nested
--- a/src/Pure/Isar/outer_lex.ML Wed Jun 07 14:19:10 2000 +0200
+++ b/src/Pure/Isar/outer_lex.ML Wed Jun 07 14:19:48 2000 +0200
@@ -170,7 +170,8 @@
val scan_str =
scan_blank ||
- keep_line ($$ "\\" |-- Scan.one (Symbol.not_sync andf Symbol.not_eof)) ||
+ keep_line ($$ "\\") |-- !! (lex_err (K "bad escape character in string"))
+ (scan_blank || keep_line ($$ "\"" || $$ "\\")) ||
keep_line (Scan.one (not_equal "\\" andf not_equal "\"" andf
Symbol.not_sync andf Symbol.not_eof));