# HG changeset patch
# User clasohm
# Date 796389197 -7200
# Node ID f7011b47ac381be1d82e483d0b9f4f9490a55867
# Parent  5d57287e5e1ec38d5e5fed84a8a76dd4bc74feff
changed string scanner so that newlines ('\n') are allowed and ignored inside
strings

diff -r 5d57287e5e1e -r f7011b47ac38 src/Pure/Thy/thy_scan.ML
--- a/src/Pure/Thy/thy_scan.ML	Tue Mar 28 12:25:20 1995 +0200
+++ b/src/Pure/Thy/thy_scan.ML	Tue Mar 28 13:13:17 1995 +0200
@@ -74,8 +74,7 @@
         (None, _) => lex_err n "bad escape sequence in string"
       | (Some s, cs') => cons_fst ("\\" ^ s) (string cs' (inc_line n s)))
   | string (c :: cs) n = 
-      if c = "\n" then 
-        lex_err n "no matching quote found on this line"
+      if c = "\n" then string cs (n+1)
       else cons_fst c (string cs n)
   | string [] n = lex_err n "missing quote at end of string";