# HG changeset patch
# User wenzelm
# Date 1660745421 -7200
# Node ID c8a8b3bff1b4a99baefbf0ee4c94e4156288dab1
# Parent  a63ccf1a583ea2d8f347ca6dd26c16648516bf16
tuned signature;

diff -r a63ccf1a583e -r c8a8b3bff1b4 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Wed Aug 17 16:07:10 2022 +0200
+++ b/src/Pure/Thy/presentation.scala	Wed Aug 17 16:10:21 2022 +0200
@@ -571,10 +571,6 @@
           map(link => HTML.text("View ") ::: List(link))).flatten
     }
 
-    def entity_context(name: Document.Node.Name): Entity_Context =
-      Entity_Context.make(session, name, html_context)
-
-
     sealed case class Seen_File(
       src_path: Path,
       thy_name: Document.Node.Name,
@@ -615,8 +611,8 @@
 
         val thy_html =
           html_context.source(
-            make_html(entity_context(name), thy_elements,
-              snapshot.xml_markup(elements = thy_elements.html)))
+            make_html(Entity_Context.make(session, name, html_context),
+              thy_elements, snapshot.xml_markup(elements = thy_elements.html)))
 
         val thy_session = html_context.theory_session_info(name).name
         val thy_dir = Isabelle_System.make_directory(html_context.theory_dir(name))