--- 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] =
--- 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 = {