# HG changeset patch
# User wenzelm
# Date 1308348238 -7200
# Node ID 5c716a68931afcc8a948297daa8cc0bc3c7c5923
# Parent  24e2e2f0032b9260ce359e2e18db69e4309c5b29
select_markup: no filtering here -- results may be distorted anyway;

diff -r 24e2e2f0032b -r 5c716a68931a src/Pure/PIDE/document.scala
--- 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)
         }
       }
     }