# HG changeset patch
# User clasohm
# Date 784820840 -3600
# Node ID 1f5800d2c366854b4217202a52ee229a84d1413a
# Parent  bb868a30e66f07e5dfe0e2f1b65cef6d352e2053
added check for newlines not enclosed by '\' inside strings

diff -r bb868a30e66f -r 1f5800d2c366 src/Pure/Thy/thy_scan.ML
--- a/src/Pure/Thy/thy_scan.ML	Mon Nov 14 14:29:20 1994 +0100
+++ b/src/Pure/Thy/thy_scan.ML	Mon Nov 14 14:47:20 1994 +0100
@@ -73,7 +73,10 @@
       (case optional scan_esc cs of
         (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 = cons_fst c (string cs n)
+  | string (c :: cs) n = 
+      if c = "\n" then 
+        lex_err n "no matching quote found on this line"
+      else cons_fst c (string cs n)
   | string [] n = lex_err n "missing quote at end of string";