Changes tabs found in .thy files to spaces
authorpaulson
Fri Nov 01 15:42:40 1996 +0100 (1996-11-01)
changeset 2151000767995143
parent 2150 084218afaf4b
child 2152 76d5ed939545
Changes tabs found in .thy files to spaces
src/Pure/Thy/thy_scan.ML
     1.1 --- a/src/Pure/Thy/thy_scan.ML	Fri Nov 01 15:41:09 1996 +0100
     1.2 +++ b/src/Pure/Thy/thy_scan.ML	Fri Nov 01 15:42:40 1996 +0100
     1.3 @@ -75,6 +75,7 @@
     1.4        | (Some s, cs') => cons_fst ("\\" ^ s) (string cs' (inc_line n s)))
     1.5    | string (c :: cs) n = 
     1.6        if c = "\n" then string cs (n+1)
     1.7 +      else if is_blank c then cons_fst " " (string cs n)
     1.8        else cons_fst c (string cs n)
     1.9    | string [] n = lex_err n "missing quote at end of string";
    1.10