# HG changeset patch
# User wenzelm
# Date 1605912817 -3600
# Node ID 4db9411c859cb682d181bce663c7655677a6c294
# Parent  5e7916535860f9b9b6b4c05a179aa3f7043ebe4b
tuned signature;

diff -r 5e7916535860 -r 4db9411c859c src/Pure/Thy/presentation.scala
--- 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)
     }
 
diff -r 5e7916535860 -r 4db9411c859c src/Pure/Thy/sessions.scala
--- 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 =