# HG changeset patch
# User wenzelm
# Date 1659527381 -7200
# Node ID b6d74c90b58876b917f4d1ba461c8f0eec8300bb
# Parent  8dc9d979bbacb50264c5fa90cd91065e40014a32
clarified signature;

diff -r 8dc9d979bbac -r b6d74c90b588 src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Wed Aug 03 13:07:32 2022 +0200
+++ b/src/Pure/Thy/document_build.scala	Wed Aug 03 13:49:41 2022 +0200
@@ -167,8 +167,10 @@
 
     def documents: List[Document_Variant] = info.documents
 
-    def session_theories: List[Document.Node.Name] = base.session_theories
-    def document_theories: List[Document.Node.Name] = session_theories ::: base.document_theories
+    def proper_session_theories: List[Document.Node.Name] = base.proper_session_theories
+
+    def document_theories: List[Document.Node.Name] =
+      proper_session_theories ::: base.document_theories
 
     lazy val document_latex: List[File.Content_XML] =
       for (name <- document_theories)
@@ -188,7 +190,7 @@
       val path = Path.basic("session.tex")
       val content =
         Library.terminate_lines(
-          base.session_theories.map(name => "\\input{" + tex_name(name) + "}"))
+          base.proper_session_theories.map(name => "\\input{" + tex_name(name) + "}"))
       File.Content(path, content)
     }
 
diff -r 8dc9d979bbac -r b6d74c90b588 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Wed Aug 03 13:07:32 2022 +0200
+++ b/src/Pure/Thy/presentation.scala	Wed Aug 03 13:49:41 2022 +0200
@@ -640,7 +640,7 @@
       }
     }
 
-    val theories = base.session_theories.flatMap(present_theory)
+    val theories = base.proper_session_theories.flatMap(present_theory)
 
     val title = "Session " + session
     HTML.write_document(session_dir, "index.html",
diff -r 8dc9d979bbac -r b6d74c90b588 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Wed Aug 03 13:07:32 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Wed Aug 03 13:49:41 2022 +0200
@@ -62,7 +62,7 @@
     pos: Position.T = Position.none,
     session_directories: Map[JFile, String] = Map.empty,
     global_theories: Map[String, String] = Map.empty,
-    session_theories: List[Document.Node.Name] = Nil,
+    proper_session_theories: List[Document.Node.Name] = Nil,
     document_theories: List[Document.Node.Name] = Nil,
     loaded_theories: Graph[String, Outer_Syntax] = Graph.string,  // cumulative imports
     used_theories: List[(Document.Node.Name, Options)] = Nil,  // new imports
@@ -172,7 +172,7 @@
 
             val overall_syntax = dependencies.overall_syntax
 
-            val session_theories =
+            val proper_session_theories =
               dependencies.theories.filter(name => deps_base.theory_qualifier(name) == session_name)
 
             val theory_files = dependencies.theories.map(_.path)
@@ -271,7 +271,7 @@
                     case None => err("Unknown document theory")
                     case Some(name) =>
                       val qualifier = deps_base.theory_qualifier(name)
-                      if (session_theories.contains(name)) {
+                      if (proper_session_theories.contains(name)) {
                         err("Redundant document theory from this session:")
                       }
                       else if (build_hierarchy.contains(qualifier)) None
@@ -286,7 +286,7 @@
               val ok = info.dirs.map(_.canonical_file).toSet
               val bad =
                 (for {
-                  name <- session_theories.iterator
+                  name <- proper_session_theories.iterator
                   path = name.master_dir_path
                   if !ok(path.canonical_file)
                   path1 = File.relative_path(info.dir.canonical, path).getOrElse(path)
@@ -302,7 +302,7 @@
               val errs3 = for (p <- info.dirs if !p.is_dir) yield "No such directory: " + p
               val errs4 =
                 (for {
-                  name <- session_theories.iterator
+                  name <- proper_session_theories.iterator
                   name1 <- resources.find_theory_node(name.theory)
                   if name.node != name1.node
                 } yield "Incoherent theory file import:\n  " + name.path + " vs. \n  " + name1.path)
@@ -327,7 +327,7 @@
                 pos = info.pos,
                 session_directories = sessions_structure.session_directories,
                 global_theories = sessions_structure.global_theories,
-                session_theories = session_theories,
+                proper_session_theories = proper_session_theories,
                 document_theories = document_theories,
                 loaded_theories = dependencies.loaded_theories,
                 used_theories = dependencies.theories_adjunct,