# HG changeset patch
# User wenzelm
# Date 1659104479 -7200
# Node ID 0c123f9c3d56dc18e1f1b9e8e9547dfdd3a9dad5
# Parent  869b1923ba44b8b60f5320258cd5020d05e1490a
tuned;

diff -r 869b1923ba44 -r 0c123f9c3d56 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Fri Jul 29 16:04:56 2022 +0200
+++ b/src/Pure/Thy/presentation.scala	Fri Jul 29 16:21:19 2022 +0200
@@ -605,13 +605,13 @@
             make_html(entity_context(name), thy_elements,
               snapshot.xml_markup(elements = thy_elements.html)))
 
-        val thy_session = html_context.theory_session(name)
+        val thy_session = html_context.theory_session(name).name
         val thy_dir = Isabelle_System.make_directory(html_context.theory_dir(name))
         val files =
           for { (src_path, file_html) <- files_html }
             yield {
-              seen_files.find(_.check(src_path, name, thy_session.name)) match {
-                case None => seen_files ::= Seen_File(src_path, name, thy_session.name)
+              seen_files.find(_.check(src_path, name, thy_session)) match {
+                case None => seen_files ::= Seen_File(src_path, name, thy_session)
                 case Some(seen_file) =>
                   error("Incoherent use of file name " + src_path + " as " + files_path(src_path) +
                     " in theory " + seen_file.thy_name + " vs. " + name)
@@ -632,7 +632,7 @@
           List(HTML.title(thy_title)), List(html_context.head(thy_title), thy_html),
           base = Some(html_context.root_dir))
 
-        if (thy_session.name == session) {
+        if (thy_session == session) {
           Some(
             List(HTML.link(html_name(name),
               HTML.text(name.theory_base_name) :::