--- a/src/Pure/Thy/presentation.scala Fri Nov 20 23:47:34 2020 +0100
+++ b/src/Pure/Thy/presentation.scala Fri Nov 20 23:53:37 2020 +0100
@@ -134,7 +134,7 @@
def enabled(info: Sessions.Info): Boolean = enabled || info.browser_info
def dir(store: Sessions.Store): Path = store.presentation_dir
def dir(store: Sessions.Store, info: Sessions.Info): Path =
- dir(store) + Path.basic(info.chapter) + Path.basic(info.name)
+ dir(store) + Path.explode(info.chapter_session)
}
@@ -277,7 +277,7 @@
val prefix =
if (session == session1) ""
else if (info.chapter == info1.chapter) "../" + session1 + "/"
- else "../../" + info1.chapter + "/" + session1 + "/"
+ else "../../" + info1.chapter_session + "/"
HTML.link(prefix + html_name(name1), body)
}
--- a/src/Pure/Thy/sessions.scala Fri Nov 20 23:47:34 2020 +0100
+++ b/src/Pure/Thy/sessions.scala Fri Nov 20 23:53:37 2020 +0100
@@ -163,7 +163,7 @@
val groups =
if (info.groups.isEmpty) ""
else info.groups.mkString(" (", " ", ")")
- progress.echo("Session " + info.chapter + "/" + info.name + groups)
+ progress.echo("Session " + info.chapter_session + groups)
}
val dependencies = resources.session_dependencies(info)
@@ -466,6 +466,8 @@
export_files: List[(Path, Int, List[String])],
meta_digest: SHA1.Digest)
{
+ def chapter_session: String = chapter + "/" + name
+
def deps: List[String] = parent.toList ::: imports
def deps_base(session_bases: String => Base): Base =