# HG changeset patch
# User wenzelm
# Date 1661011153 -7200
# Node ID 811092261546cec5303b39915a0595be85f55c3d
# Parent  fa8d9e5ef9130399e6438f6b2810cb82147149e6
proper node_dir within presentation_dir, not source file directory;

diff -r fa8d9e5ef913 -r 811092261546 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Sat Aug 20 17:25:55 2022 +0200
+++ b/src/Pure/Thy/presentation.scala	Sat Aug 20 17:59:13 2022 +0200
@@ -145,11 +145,11 @@
       html_context: HTML_Context,
       session_name: String,
       theory_name: String,
-      file_name: String
+      file_name: String,
+      node_dir: Path,
     ): Node_Context =
       new Node_Context {
         private val session_dir = html_context.session_dir(session_name)
-        private val file_dir = Path.explode(file_name).dir
 
         private val seen_ranges: mutable.Set[Symbol.Range] = mutable.Set.empty
 
@@ -180,7 +180,7 @@
               for (theory <- html_context.theory_by_name(session_name, thy_name))
               yield {
                 val html_path = session_dir + html_context.theory_html(theory)
-                val html_link = html_context.relative_link(file_dir, html_path)
+                val html_link = html_context.relative_link(node_dir, html_path)
                 HTML.link(html_link, body)
               }
             case Entity_Ref(def_file, kind, name) =>
@@ -201,7 +201,7 @@
               }
               yield {
                 val html_path = session_dir + html_context.smart_html(theory, def_file)
-                val html_link = html_context.relative_link(file_dir, html_path)
+                val html_link = html_context.relative_link(node_dir, html_path)
                 HTML.entity_ref(HTML.link(html_link + "#" + html_ref, body))
               }
             case _ => None
@@ -495,12 +495,12 @@
 
       val thy_elements = theory.elements(html_context.elements)
 
-      def node_context(file_name: String): Node_Context =
-        Node_Context.make(html_context, session_name, theory_name, file_name)
+      def node_context(file_name: String, node_dir: Path): Node_Context =
+        Node_Context.make(html_context, session_name, theory_name, file_name, node_dir)
 
       val thy_html =
         html_context.source(
-          node_context(theory.thy_file).
+          node_context(theory.thy_file, session_dir).
             make_html(thy_elements, snapshot.xml_markup(elements = thy_elements.html)))
 
       val blobs_html =