# HG changeset patch
# User wenzelm
# Date 1332788610 -7200
# Node ID 89b13238d7f24f257eaf2f49c4b1480f9fa3f819
# Parent  bef6bc52a32e5d3268639fb8996774b2d5077a37# Parent  0e45e363306c72a95c52144d2243851e62bb70b9
merged

diff -r bef6bc52a32e -r 89b13238d7f2 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Mon Mar 26 21:00:39 2012 +0200
+++ b/src/Pure/General/symbol.scala	Mon Mar 26 21:03:30 2012 +0200
@@ -347,7 +347,7 @@
       "\\<^isub>", "\\<^isup>")
 
     val blanks =
-      recode_set(space, "\t", "\n", "\u000B", "\f", "\r", "\\<spacespace>", "\\<^newline>")
+      recode_set(space, "\t", "\n", "\u000B", "\f", "\r", "\r\n", "\\<spacespace>", "\\<^newline>")
 
     val sym_chars =
       Set("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~")