# HG changeset patch
# User wenzelm
# Date 1672774491 -3600
# Node ID 1c3bf6e5f73f48da80603592c017813016131fd5
# Parent  d8cdddf7b9a5cf7d62870044a3ddd64052471376
tuned;

diff -r d8cdddf7b9a5 -r 1c3bf6e5f73f src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Jan 03 17:21:24 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Tue Jan 03 20:34:51 2023 +0100
@@ -363,9 +363,12 @@
                 theory -> files.map(file => Path.explode(file.node))
               }
 
+            val document_files =
+              for ((path1, path2) <- info.document_files)
+                yield info.dir + path1 + path2
+
             val session_files =
-              (theory_files ::: loaded_files.flatMap(_._2) :::
-                info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand)
+              (theory_files ::: loaded_files.flatMap(_._2) ::: document_files).map(_.expand)
 
             val imported_files = if (inlined_files) dependencies.imported_files else Nil