changeset 2151 | 000767995143 |
parent 1512 | ce37c64244c0 |
child 2204 | 64cb98f841e4 |
--- a/src/Pure/Thy/thy_scan.ML Fri Nov 01 15:41:09 1996 +0100 +++ b/src/Pure/Thy/thy_scan.ML Fri Nov 01 15:42:40 1996 +0100 @@ -75,6 +75,7 @@ | (Some s, cs') => cons_fst ("\\" ^ s) (string cs' (inc_line n s))) | string (c :: cs) n = if c = "\n" then string cs (n+1) + else if is_blank c then cons_fst " " (string cs n) else cons_fst c (string cs n) | string [] n = lex_err n "missing quote at end of string";