more robust: ensure that chapter/session/theory do not contain special notation (like "/" or "..");
--- 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)
}
--- 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 = {