changed string scanner so that newlines ('\n') are allowed and ignored inside
authorclasohm
Tue, 28 Mar 1995 13:13:17 +0200
changeset 978f7011b47ac38
parent 977 5d57287e5e1e
child 979 a29142d703bc
changed string scanner so that newlines ('\n') are allowed and ignored inside
strings
src/Pure/Thy/thy_scan.ML
     1.1 --- a/src/Pure/Thy/thy_scan.ML	Tue Mar 28 12:25:20 1995 +0200
     1.2 +++ b/src/Pure/Thy/thy_scan.ML	Tue Mar 28 13:13:17 1995 +0200
     1.3 @@ -74,8 +74,7 @@
     1.4          (None, _) => lex_err n "bad escape sequence in string"
     1.5        | (Some s, cs') => cons_fst ("\\" ^ s) (string cs' (inc_line n s)))
     1.6    | string (c :: cs) n = 
     1.7 -      if c = "\n" then 
     1.8 -        lex_err n "no matching quote found on this line"
     1.9 +      if c = "\n" then string cs (n+1)
    1.10        else cons_fst c (string cs n)
    1.11    | string [] n = lex_err n "missing quote at end of string";
    1.12