diff -r 6623c81cb15a -r 634cd44bb1d3 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Wed Nov 04 23:27:00 2015 +0100
+++ b/src/Pure/PIDE/command.scala	Thu Nov 05 00:02:30 2015 +0100
@@ -308,10 +308,11 @@
 
   private def clean_tokens(tokens: List[Token]): List[(Token, Int)] =
   {
+    val markers = Set("%", "--", Symbol.comment, Symbol.comment_decoded)
     def clean(toks: List[(Token, Int)]): List[(Token, Int)] =
       toks match {
         case (t1, i1) :: (t2, i2) :: rest =>
-          if (t1.is_keyword && (t1.source == "%" || t1.source == "--")) clean(rest)
+          if (t1.is_keyword && markers(t1.source)) clean(rest)
           else (t1, i1) :: clean((t2, i2) :: rest)
         case _ => toks
       }