# HG changeset patch
# User wenzelm
# Date 1636208720 -3600
# Node ID 129fb11b357fec75513dbc458f6c82ab44999dff
# Parent  1357876014383e5a0d9b93e4f5847cec50f04eb6
use all entity kinds from theory export, e.g. "method", "attribute";

diff -r 135787601438 -r 129fb11b357f src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Sat Nov 06 11:25:03 2021 +0100
+++ b/src/Pure/Thy/presentation.scala	Sat Nov 06 15:25:20 2021 +0100
@@ -85,8 +85,7 @@
     Elements(
       html = Rendering.foreground_elements ++ Rendering.text_color_elements +
         Markup.NUMERAL + Markup.COMMENT + Markup.ENTITY + Markup.LANGUAGE,
-      entity = Markup.Elements(Markup.THEORY, Markup.TYPE_NAME, Markup.CONSTANT, Markup.FACT,
-        Markup.CLASS, Markup.LOCALE, Markup.FREE))
+      entity = Markup.Elements(Markup.THEORY, Markup.FREE))
 
   val elements2: Elements =
     Elements(
@@ -384,7 +383,7 @@
     progress: Progress = new Progress,
     verbose: Boolean = false,
     html_context: HTML_Context,
-    elements: Elements,
+    session_elements: Elements,
     presentation: Context): Unit =
   {
     val hierarchy = deps.sessions_structure.hierarchy(session)
@@ -543,9 +542,13 @@
           if (verbose) progress.echo("Presenting theory " + name)
           val snapshot = Document.State.init.snippet(command)
 
+          val thy_elements =
+            session_elements.copy(entity =
+              theory_exports(name.theory).entity_kinds.foldLeft(session_elements.entity)(_ + _))
+
           val files_html =
             for {
-              (src_path, xml) <- snapshot.xml_markup_blobs(elements = elements.html)
+              (src_path, xml) <- snapshot.xml_markup_blobs(elements = thy_elements.html)
               if xml.nonEmpty
             }
             yield {
@@ -553,13 +556,13 @@
               if (verbose) progress.echo("Presenting file " + src_path)
 
               (src_path, html_context.source(
-                make_html(name, elements, entity_anchor, entity_link, xml)))
+                make_html(name, thy_elements, entity_anchor, entity_link, xml)))
             }
 
           val html =
             html_context.source(
-              make_html(name, elements, entity_anchor, entity_link,
-                snapshot.xml_markup(elements = elements.html)))
+              make_html(name, thy_elements, entity_anchor, entity_link,
+                snapshot.xml_markup(elements = thy_elements.html)))
 
           Theory(name, command, files_html, html)
         }
diff -r 135787601438 -r 129fb11b357f src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Nov 06 11:25:03 2021 +0100
+++ b/src/Pure/Tools/build.scala	Sat Nov 06 15:25:20 2021 +0100
@@ -516,7 +516,7 @@
             Presentation.session_html(
               resources, info.name, deps, db_context, progress = progress,
               verbose = verbose, html_context = html_context,
-              elements = Presentation.elements1, presentation = presentation)
+              Presentation.elements1, presentation = presentation)
           })
       }
     }