cover all possible kinds, notably for references outside of this theory (amending 129fb11b357f);
authorwenzelm
Sat, 06 Nov 2021 19:47:56 +0100
changeset 74718 925b46043b84
parent 74717 baed95c97505
child 74719 d274100827b0
cover all possible kinds, notably for references outside of this theory (amending 129fb11b357f);
src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Sat Nov 06 19:17:51 2021 +0100
+++ b/src/Pure/Thy/presentation.scala	Sat Nov 06 19:47:56 2021 +0100
@@ -85,7 +85,8 @@
     Elements(
       html = Rendering.foreground_elements ++ Rendering.text_color_elements +
         Markup.NUMERAL + Markup.COMMENT + Markup.ENTITY + Markup.LANGUAGE,
-      entity = Markup.Elements(Markup.THEORY, Markup.FREE))
+      entity = Markup.Elements(Markup.THEORY, Markup.TYPE_NAME, Markup.CONSTANT, Markup.FACT,
+        Markup.CLASS, Markup.LOCALE, Markup.FREE))
 
   val elements2: Elements =
     Elements(
@@ -547,7 +548,7 @@
 
           val thy_elements =
             session_elements.copy(entity =
-              theory_exports(name.theory).entity_kinds.foldLeft(session_elements.entity)(_ + _))
+              theory_exports(name.theory).others.keySet.foldLeft(session_elements.entity)(_ + _))
 
           val files_html =
             for {