select_markup: no filtering here -- results may be distorted anyway;

--- a/src/Pure/PIDE/document.scala	Fri Jun 17 23:20:34 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Sat Jun 18 00:03:58 2011 +0200
@@ -322,9 +322,7 @@
                 if result.isDefinedAt(Text.Info(convert(r0 + command_start), info)) =>
                   result(Text.Info(convert(r0 + command_start), info))
               }
-            val r = convert(r0 + command_start)
-            if !r.is_singularity
-          } yield Text.Info(r, x)
+          } yield Text.Info(convert(r0 + command_start), x)
         }
       }
     }