src/Pure/PIDE/rendering.scala
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