improved string scanner: converts 8 bit chars to escape sequences;
authorwenzelm
Mon Nov 18 17:32:38 1996 +0100 (1996-11-18)
changeset 220464cb98f841e4
parent 2203 c2dbdc2ef781
child 2205 c5a7c72746ac
improved string scanner: converts 8 bit chars to escape sequences;
src/Pure/Thy/thy_scan.ML
     1.1 --- a/src/Pure/Thy/thy_scan.ML	Mon Nov 18 17:31:14 1996 +0100
     1.2 +++ b/src/Pure/Thy/thy_scan.ML	Mon Nov 18 17:32:38 1996 +0100
     1.3 @@ -73,10 +73,11 @@
     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 ("\n" :: cs) n = cons_fst " " (string cs (n + 1))
     1.8    | string (c :: cs) n = 
     1.9 -      if c = "\n" then string cs (n+1)
    1.10 -      else if is_blank c then cons_fst " " (string cs n)
    1.11 -      else cons_fst c (string cs n)
    1.12 +      if is_blank c then cons_fst " " (string cs n)
    1.13 +      else if is_printable c then cons_fst c (string cs n)
    1.14 +      else cons_fst ("\\" ^ string_of_int (ord c)) (string cs n)
    1.15    | string [] n = lex_err n "missing quote at end of string";
    1.16  
    1.17