src/Pure/PIDE/command.scala
changeset 61579 634cd44bb1d3
parent 61197 b9d69001824e
child 62965 5bf08c9aa036
     1.1 --- a/src/Pure/PIDE/command.scala	Wed Nov 04 23:27:00 2015 +0100
     1.2 +++ b/src/Pure/PIDE/command.scala	Thu Nov 05 00:02:30 2015 +0100
     1.3 @@ -308,10 +308,11 @@
     1.4  
     1.5    private def clean_tokens(tokens: List[Token]): List[(Token, Int)] =
     1.6    {
     1.7 +    val markers = Set("%", "--", Symbol.comment, Symbol.comment_decoded)
     1.8      def clean(toks: List[(Token, Int)]): List[(Token, Int)] =
     1.9        toks match {
    1.10          case (t1, i1) :: (t2, i2) :: rest =>
    1.11 -          if (t1.is_keyword && (t1.source == "%" || t1.source == "--")) clean(rest)
    1.12 +          if (t1.is_keyword && markers(t1.source)) clean(rest)
    1.13            else (t1, i1) :: clean((t2, i2) :: rest)
    1.14          case _ => toks
    1.15        }