avoid broken links: auxiliary files are not yet supported;
authorwenzelm
Thu, 25 Nov 2021 12:36:54 +0100
changeset 74841 9ad3fa47c83e
parent 74840 4faf0ec33cbf
child 74842 29672359a371
avoid broken links: auxiliary files are not yet supported;
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 =