| changeset 69887 | b9985133805d |
| parent 69634 | 70f1994988d4 |
| child 69891 | def3ec9cdb7e |
--- a/src/Pure/PIDE/command.scala Sat Mar 09 23:57:07 2019 +0100 +++ b/src/Pure/PIDE/command.scala Sun Mar 10 00:21:34 2019 +0100 @@ -475,6 +475,7 @@ toks match { case (t1, i1) :: (t2, i2) :: rest => if (t1.is_keyword && t1.source == "%" && t2.is_name) clean(rest) + else if (t1.is_keyword && Symbol.is_marker(t1.source) && t2.is_embedded) clean(rest) else (t1, i1) :: clean((t2, i2) :: rest) case _ => toks }