# HG changeset patch
# User wenzelm
# Date 1636629377 -3600
# Node ID 0dbb6b50e0631c52467b1061b6b4868b5e4f0a5f
# Parent  95643a0bff4950dcc36f8ba2bdc2189cbd6bf91a
more hyperlinks, notably internal fact references;

diff -r 95643a0bff49 -r 0dbb6b50e063 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Wed Nov 10 19:45:30 2021 +0100
+++ b/src/Pure/Thy/presentation.scala	Thu Nov 11 12:16:17 2021 +0100
@@ -516,11 +516,15 @@
             val node_name = resources.file_node(Path.explode(thy_file), theory = theory)
             node_relative(deps, session, node_name).map(html_dir =>
               HTML.link(html_dir + html_name(node_name), body))
-          case (Markup.Ref(_), Position.Def_File(thy_file), Position.Def_Theory(def_theory),
+          case (Markup.Ref(_), Position.Def_File(def_file), Position.Def_Theory(def_theory),
               Markup.Kind(kind), Markup.Name(name)) =>
-            val thy_name = if (def_theory.nonEmpty) def_theory else context.node.theory
-            val node_name = resources.file_node(Path.explode(thy_file), theory = thy_name)
+            val file_path = Path.explode(def_file)
+            val proper_thy_name =
+              proper_string(def_theory) orElse
+                (if (File.eq(context.node.path, file_path)) Some(context.node.theory) else None)
             for {
+              thy_name <- proper_thy_name
+              node_name = resources.file_node(file_path, theory = thy_name)
               html_dir <- node_relative(deps, session, node_name)
               html_file = node_file(node_name)
               html_ref <-