# HG changeset patch
# User wenzelm
# Date 960380388 -7200
# Node ID 887a15590f0e82f427316c3aec44039ca87f6079
# Parent  5787308106387f4fc531754e400bbdf8d998c131
string syntax: allow \\ \" \\n only;

diff -r 578730810638 -r 887a15590f0e doc-src/IsarRef/syntax.tex
--- 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
diff -r 578730810638 -r 887a15590f0e src/Pure/Isar/outer_lex.ML
--- 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));