# HG changeset patch
# User wenzelm
# Date 1661506919 -7200
# Node ID 59aa034220bfda9eaee044a967ea5950672441a6
# Parent  3acc90a2ef6d480f18c5b12d8232520cae7ab46c
more robust: ensure that chapter/session/theory do not contain special notation (like "/" or "..");

diff -r 3acc90a2ef6d -r 59aa034220bf src/Pure/Thy/browser_info.scala
--- a/src/Pure/Thy/browser_info.scala	Thu Aug 25 23:09:00 2022 +0200
+++ b/src/Pure/Thy/browser_info.scala	Fri Aug 26 11:41:59 2022 +0200
@@ -183,7 +183,7 @@
       document_info.theory_by_file(session, file)
 
     def session_dir(session: String): Path =
-      root_dir + Path.explode(sessions_structure(session).chapter_session)
+      root_dir + Path.basic(sessions_structure(session).chapter) + Path.basic(session)
 
     def chapter_dir(chapter: String): Path =
       root_dir + Path.basic(chapter)
@@ -194,7 +194,7 @@
     def theory_html(theory: Document_Info.Theory): Path =
     {
       def check(name: String): Option[Path] = {
-        val path = Path.explode(name).html
+        val path = Path.basic(name).html
         if (Path.eq_case_insensitive(path, Path.index_html)) None
         else Some(path)
       }
diff -r 3acc90a2ef6d -r 59aa034220bf src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Aug 25 23:09:00 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri Aug 26 11:41:59 2022 +0200
@@ -167,7 +167,7 @@
               val groups =
                 if (info.groups.isEmpty) ""
                 else info.groups.mkString(" (", " ", ")")
-              progress.echo("Session " + info.chapter_session + groups)
+              progress.echo("Session " + info.chapter + "/" + session_name + groups)
             }
 
             val dependencies = resources.session_dependencies(info)
@@ -477,8 +477,6 @@
     export_classpath: 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 = {