equal
deleted
inserted
replaced
181 fun is_quasi_letter "_" = true |
181 fun is_quasi_letter "_" = true |
182 | is_quasi_letter "'" = true |
182 | is_quasi_letter "'" = true |
183 | is_quasi_letter s = is_letter s; |
183 | is_quasi_letter s = is_letter s; |
184 |
184 |
185 val is_blank = |
185 val is_blank = |
186 fn " " => true | "\t" => true | "\n" => true | "\^L" => true | "\\<space2>" => true |
186 fn " " => true | "\t" => true | "\n" => true | "\^L" => true |
|
187 | "\160" => true | "\\<space2>" => true |
187 | _ => false; |
188 | _ => false; |
188 |
189 |
189 val is_letdig = is_quasi_letter orf is_digit; |
190 val is_letdig = is_quasi_letter orf is_digit; |
190 |
191 |
191 fun is_printable s = |
192 fun is_printable s = |