# HG changeset patch
# User wenzelm
# Date 1466522517 -7200
# Node ID 29d7ac9bdcb16038e24deaff478fa93d32d71827
# Parent  fd9bd5024751dead71d650e2ba68d2844e70d435
clarified rendering (amending ae9330fdbc16);

diff -r fd9bd5024751 -r 29d7ac9bdcb1 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Tue Jun 21 16:10:03 2016 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Tue Jun 21 17:21:57 2016 +0200
@@ -600,7 +600,11 @@
           case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
             Some(Text.Info(r, (t1 + t2, info)))
 
-          case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _))) =>
+          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 =>
             val kind1 = Word.implode(Word.explode('_', kind))
             val txt1 =
               if (name == "") kind1