# HG changeset patch
# User wenzelm
# Date 1637840214 -3600
# Node ID 9ad3fa47c83eefdb9cb6329b79fcb6b05deb7f10
# Parent  4faf0ec33cbf1160dd270637e66e27d7764712b7
avoid broken links: auxiliary files are not yet supported;

diff -r 4faf0ec33cbf -r 9ad3fa47c83e src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Wed Nov 24 22:57:33 2021 +0100
+++ b/src/Pure/Thy/presentation.scala	Thu Nov 25 12:36:54 2021 +0100
@@ -182,7 +182,7 @@
             case Theory_Ref(node_name) =>
               node_relative(deps, session, node_name).map(html_dir =>
                 HTML.link(html_dir + html_name(node_name), body))
-            case Entity_Ref(file_path, def_theory, kind, name) =>
+            case Entity_Ref(file_path, def_theory, kind, name) if file_path.get_ext == "thy" =>
               for {
                 thy_name <-
                   def_theory orElse (if (File.eq(node.path, file_path)) Some(node.theory) else None)
@@ -604,7 +604,7 @@
             if (verbose) progress.echo("Presenting file " + src_path)
 
             (src_path, html_context.source(
-              make_html(entity_context(name), thy_elements, xml)))
+              make_html(Entity_Context.empty, thy_elements, xml)))
           }
 
         val thy_html =