| changeset 14221 | 9276f30eaed6 |
| parent 14173 | a3690aeb79d4 |
| child 14232 | ef550525c591 |
--- a/src/Pure/General/symbol.ML Wed Oct 08 15:57:41 2003 +0200 +++ b/src/Pure/General/symbol.ML Wed Oct 08 15:58:15 2003 +0200 @@ -137,7 +137,7 @@ fun is_quasi_letter s = is_quasi s orelse is_letter s; val is_blank = - fn " " => true | "\t" => true | "\n" => true | "\^L" => true + fn " " => true | "\t" => true | "\r" => true | "\n" => true | "\^L" => true | "\160" => true | "\\<spacespace>" => true | _ => false;