# HG changeset patch
# User wenzelm
# Date 1332787559 -7200
# Node ID 0e45e363306c72a95c52144d2243851e62bb70b9
# Parent  bd1679890503fa1a119079b2f0dd30444b3a19aa# Parent  fb5764df8a9cb931d9101815620beddca14824a5
merged

diff -r bd1679890503 -r 0e45e363306c src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Mon Mar 26 20:11:27 2012 +0200
+++ b/src/Pure/General/symbol.scala	Mon Mar 26 20:45:59 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("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~")