# HG changeset patch
# User wenzelm
# Date 1661508629 -7200
# Node ID a1b131d5575fdee5fb4686cc03ab986038abcf6a
# Parent  232beef27a1772fa066a8ae8d59939958fafc14c
clarified signature;

diff -r 232beef27a17 -r a1b131d5575f src/Pure/Thy/browser_info.scala
--- a/src/Pure/Thy/browser_info.scala	Fri Aug 26 12:07:24 2022 +0200
+++ b/src/Pure/Thy/browser_info.scala	Fri Aug 26 12:10:29 2022 +0200
@@ -185,11 +185,11 @@
     def session_chapter(session: String): String =
       sessions_structure(session).chapter
 
-    def session_dir(session: String): Path =
-      root_dir + Path.basic(session_chapter(session)) + Path.basic(session)
+    def chapter_dir(session: String): Path =
+      root_dir + Path.basic(session_chapter(session))
 
-    def chapter_dir(chapter: String): Path =
-      root_dir + Path.basic(chapter)
+    def session_dir(session: String): Path =
+      chapter_dir(session) + Path.basic(session)
 
     def theory_dir(theory: Document_Info.Theory): Path =
       session_dir(theory.dynamic_session)
@@ -273,8 +273,7 @@
     /* maintain presentation structure */
 
     def update_chapter(session_name: String, session_description: String): Unit = synchronized {
-      val chapter = session_chapter(session_name)
-      val dir = Meta_Data.init_directory(chapter_dir(chapter))
+      val dir = Meta_Data.init_directory(chapter_dir(session_name))
       Meta_Data.change(dir, Meta_Data.INDEX) { text =>
         val index0 = Meta_Data.Index.parse(text, "chapter")
         val item = Meta_Data.Item(session_name, description = session_description)
@@ -282,7 +281,7 @@
         val sessions = index.items
 
         if (index != index0) {
-          val title = "Isabelle/" + chapter + " sessions"
+          val title = "Isabelle/" + session_chapter(session_name) + " sessions"
           HTML.write_document(dir, "index.html",
             List(HTML.title(title + Isabelle_System.isabelle_heading())),
             HTML.chapter(title) ::
@@ -532,7 +531,7 @@
     val session_dir = context.session_dir(session_name).expand
     progress.echo("Presenting " + session_name + " in " + session_dir + " ...")
 
-    Meta_Data.init_directory(context.chapter_dir(session_info.chapter))
+    Meta_Data.init_directory(context.chapter_dir(session_name))
     Meta_Data.init_directory(session_dir)
 
     val session = context.document_info.the_session(session_name)