| changeset 64660 | ef85bb6491b3 | 
| parent 64654 | 31b681e38c70 | 
| child 64676 | fd2df1ea3bb4 | 
--- a/src/Pure/PIDE/rendering.scala Fri Dec 23 11:19:28 2016 +0100 +++ b/src/Pure/PIDE/rendering.scala Fri Dec 23 11:21:38 2016 +0100 @@ -64,10 +64,7 @@ Some(Text.Info(r, (t1 + t2, info))) case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _))) - if kind != "" && - kind != Markup.ML_DEF && - kind != Markup.ML_OPEN && - kind != Markup.ML_STRUCTURE => + if kind != "" && kind != Markup.ML_DEF => val kind1 = Word.implode(Word.explode('_', kind)) val txt1 = if (name == "") kind1