changed string scanner so that newlines ('\n') are allowed and ignored inside
strings
--- 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";