# HG changeset patch
# User wenzelm
# Date 1604867228 -3600
# Node ID ed5b907bbf50a7f1b0563c5b319781abe57c2a3a
# Parent  6d54efe5b6eedc0309a32e28cd1b677eb2c11c4a
tuned;

diff -r 6d54efe5b6ee -r ed5b907bbf50 src/Pure/Thy/present.scala
--- a/src/Pure/Thy/present.scala	Sun Nov 08 16:20:39 2020 +0100
+++ b/src/Pure/Thy/present.scala	Sun Nov 08 21:27:08 2020 +0100
@@ -193,6 +193,17 @@
 
 
 
+  /** make document source **/
+
+  def write_tex_index(dir: Path, names: List[Document.Node.Name])
+  {
+    val path = dir + Path.explode("session.tex")
+    val text = names.map(name => "\\input{" + name.theory_base_name + ".tex}\n\n").mkString
+    File.write(path, text)
+  }
+
+
+
   /** build document **/
 
   val document_format = "pdf"
diff -r 6d54efe5b6ee -r ed5b907bbf50 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sun Nov 08 16:20:39 2020 +0100
+++ b/src/Pure/Thy/sessions.scala	Sun Nov 08 21:27:08 2020 +0100
@@ -167,10 +167,7 @@
             val overall_syntax = dependencies.overall_syntax
 
             val session_theories =
-              for {
-                name <- dependencies.theories
-                if deps_base.theory_qualifier(name) == info.name
-              } yield name
+              dependencies.theories.filter(name => deps_base.theory_qualifier(name) == session_name)
 
             val theory_files = dependencies.theories.map(_.path)
 
@@ -240,9 +237,6 @@
 
             val known_loaded_files = deps_base.known_loaded_files ++ loaded_files
 
-            val used_theories_session =
-              dependencies.theories.filter(name => deps_base.theory_qualifier(name) == session_name)
-
             val import_errors =
             {
               val known_sessions =
@@ -260,7 +254,7 @@
               val ok = info.dirs.map(_.canonical_file).toSet
               val bad =
                 (for {
-                  name <- used_theories_session.iterator
+                  name <- session_theories.iterator
                   path = name.master_dir_path
                   if !ok(path.canonical_file)
                   path1 = File.relative_path(info.dir.canonical, path).getOrElse(path)
@@ -276,7 +270,7 @@
               val errs3 = for (p <- info.dirs if !p.is_dir) yield "No such directory: " + p
               val errs4 =
                 (for {
-                  name <- used_theories_session.iterator
+                  name <- 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)
diff -r 6d54efe5b6ee -r ed5b907bbf50 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun Nov 08 16:20:39 2020 +0100
+++ b/src/Pure/Tools/build.scala	Sun Nov 08 21:27:08 2020 +0100
@@ -415,9 +415,7 @@
         for (document_output <- proper_string(options.string("document_output"))) {
           val document_output_dir =
             Isabelle_System.make_directory(info.dir + Path.explode(document_output))
-          val base = deps(session_name)
-          File.write(document_output_dir + Path.explode("session.tex"),
-            base.session_theories.map(name => "\\input{" + name.theory_base_name + ".tex}\n\n").mkString)
+          Present.write_tex_index(document_output_dir, deps(session_name).session_theories)
         }
         Present.finish(progress, store.browser_info, graph_file, info, session_name)
       }