# HG changeset patch # User wenzelm # Date 1660745783 -7200 # Node ID 2b7841f71e24f2d1c1636a05735284a9b25cb9a0 # Parent c8a8b3bff1b4a99baefbf0ee4c94e4156288dab1 tuned signature; diff -r c8a8b3bff1b4 -r 2b7841f71e24 src/Pure/Thy/presentation.scala --- a/src/Pure/Thy/presentation.scala Wed Aug 17 16:10:21 2022 +0200 +++ b/src/Pure/Thy/presentation.scala Wed Aug 17 16:16:23 2022 +0200 @@ -30,8 +30,10 @@ ) { /* directory structure and resources */ + def theory_session(name: Document.Node.Name): String = + sessions_structure.theory_qualifier(name) def theory_session_info(name: Document.Node.Name): Sessions.Info = - sessions_structure(sessions_structure.theory_qualifier(name)) + sessions_structure(theory_session(name)) def session_dir(info: Sessions.Info): Path = root_dir + Path.explode(info.chapter_session) @@ -614,7 +616,7 @@ make_html(Entity_Context.make(session, name, html_context), thy_elements, snapshot.xml_markup(elements = thy_elements.html))) - val thy_session = html_context.theory_session_info(name).name + val thy_session = html_context.theory_session(name) val thy_dir = Isabelle_System.make_directory(html_context.theory_dir(name)) val files = for { (src_path, file_html) <- files_html }