src/Pure/Thy/thy_scan.ML
changeset 712 1f5800d2c366
parent 388 dcf6c0774075
child 978 f7011b47ac38
     1.1 --- a/src/Pure/Thy/thy_scan.ML	Mon Nov 14 14:29:20 1994 +0100
     1.2 +++ b/src/Pure/Thy/thy_scan.ML	Mon Nov 14 14:47:20 1994 +0100
     1.3 @@ -73,7 +73,10 @@
     1.4        (case optional scan_esc cs of
     1.5          (None, _) => lex_err n "bad escape sequence in string"
     1.6        | (Some s, cs') => cons_fst ("\\" ^ s) (string cs' (inc_line n s)))
     1.7 -  | string (c :: cs) n = cons_fst c (string cs n)
     1.8 +  | string (c :: cs) n = 
     1.9 +      if c = "\n" then 
    1.10 +        lex_err n "no matching quote found on this line"
    1.11 +      else cons_fst c (string cs n)
    1.12    | string [] n = lex_err n "missing quote at end of string";
    1.13  
    1.14