Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clarified rendering (amending ae9330fdbc16);
authorwenzelm
Tue, 21 Jun 2016 17:21:57 +0200
changeset 63340 29d7ac9bdcb1
parent 63339 fd9bd5024751
child 63341 40f58bb9c846
clarified rendering (amending ae9330fdbc16);
src/Tools/jEdit/src/rendering.scala file | annotate | diff | comparison | revisions 
--- 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
isabelle