# HG changeset patch
# User wenzelm
# Date 1661079226 -7200
# Node ID 82739e4c1e5472dcd843d6efeed4fe34855de1f9
# Parent  c7ee4d140c8046b1591147295a54850fabef9075
proper theory_dir for links to other session;

diff -r c7ee4d140c80 -r 82739e4c1e54 src/Pure/Thy/browser_info.scala
--- a/src/Pure/Thy/browser_info.scala	Sun Aug 21 12:41:16 2022 +0200
+++ b/src/Pure/Thy/browser_info.scala	Sun Aug 21 12:53:46 2022 +0200
@@ -83,6 +83,9 @@
     def session_dir(session: String): Path =
       root_dir + Path.explode(sessions_structure(session).chapter_session)
 
+    def theory_dir(theory: Document_Info.Theory): Path =
+      session_dir(theory.dynamic_session)
+
     def theory_html(theory: Document_Info.Theory): Path =
     {
       def check(name: String): Option[Path] = {
@@ -192,8 +195,6 @@
       node_dir: Path,
     ): Node_Context =
       new Node_Context {
-        private val session_dir = context.session_dir(session_name)
-
         private val seen_ranges: mutable.Set[Symbol.Range] = mutable.Set.empty
 
         override def make_def(range: Symbol.Range, body: XML.Body): Option[XML.Elem] =
@@ -222,7 +223,7 @@
             case Theory_Ref(thy_name) =>
               for (theory <- context.theory_by_name(session_name, thy_name))
               yield {
-                val html_path = session_dir + context.theory_html(theory)
+                val html_path = context.theory_dir(theory) + context.theory_html(theory)
                 val html_link = HTML.relative_href(html_path, base = Some(node_dir))
                 HTML.link(html_link, body)
               }
@@ -243,7 +244,7 @@
                 html_ref <- logical_ref(theory) orElse physical_ref(theory)
               }
               yield {
-                val html_path = session_dir + context.smart_html(theory, def_file)
+                val html_path = context.theory_dir(theory) + context.smart_html(theory, def_file)
                 val html_link = HTML.relative_href(html_path, base = Some(node_dir))
                 HTML.entity_ref(HTML.link(html_link + "#" + html_ref, body))
               }