# 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