# HG changeset patch
# User wenzelm
# Date 1660745016 -7200
# Node ID a1336e2d768074229c30f62a7e8e27c5ea91f5e3
# Parent  ffa97500a1acb0b0fe2c6d54cf69b87026614901
clarified modules;

diff -r ffa97500a1ac -r a1336e2d7680 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Wed Aug 17 15:56:04 2022 +0200
+++ b/src/Pure/Thy/presentation.scala	Wed Aug 17 16:03:36 2022 +0200
@@ -44,7 +44,11 @@
       for {
         info0 <- sessions_structure.get(session0)
         info1 <- sessions_structure.get(session1)
-      } yield info0.relative_path(info1)
+      } yield {
+        if (info0.name == info1.name) ""
+        else if (info0.chapter == info1.chapter) "../" + info1.name + "/"
+        else "../../" + info1.chapter_session + "/"
+      }
     }
 
     def node_relative(session0: String, node_name: Document.Node.Name): Option[String] =
diff -r ffa97500a1ac -r a1336e2d7680 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Wed Aug 17 15:56:04 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Wed Aug 17 16:03:36 2022 +0200
@@ -478,11 +478,6 @@
   ) {
     def chapter_session: String = chapter + "/" + name
 
-    def relative_path(info1: Info): String =
-      if (name == info1.name) ""
-      else if (chapter == info1.chapter) "../" + info1.name + "/"
-      else "../../" + info1.chapter_session + "/"
-
     def deps: List[String] = parent.toList ::: imports
 
     def deps_base(session_bases: String => Base): Base = {