# HG changeset patch
# User paulson
# Date 1065621495 -7200
# Node ID 9276f30eaed61c83924dc45c300903a1b7751382
# Parent  4dc1329026729120b8f79ed172fb8dadbd5ddf2e
now accepts DOS and Mac line breaks

diff -r 4dc132902672 -r 9276f30eaed6 src/Pure/General/symbol.ML
--- 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;