# HG changeset patch
# User wenzelm
# Date 1660913618 -7200
# Node ID 475fedc027377044f9831a8fd6efff1e9f543268
# Parent  53342c15f979bb5a65dde1971254f589efff8f7b
clarified signature;

diff -r 53342c15f979 -r 475fedc02737 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Thu Aug 18 14:16:36 2022 +0200
+++ b/src/Pure/Thy/export.scala	Fri Aug 19 14:53:38 2022 +0200
@@ -449,10 +449,13 @@
         case _ => None
       }
 
-    def files(): Option[(String, List[String])] =
-      split_lines(apply(FILES, permissive = true).text) match {
+    def files0(permissive: Boolean = false): List[String] =
+      split_lines(apply(FILES, permissive = permissive).text)
+
+    def files(permissive: Boolean = false): Option[(String, List[String])] =
+      files0(permissive = permissive) match {
         case Nil => None
-        case thy_file :: blobs_files => Some((thy_file, blobs_files))
+        case a :: bs => Some((a, bs))
       }
 
     override def toString: String = "Export.Theory_Context(" + quote(theory) + ")"
diff -r 53342c15f979 -r 475fedc02737 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Thu Aug 18 14:16:36 2022 +0200
+++ b/src/Pure/Thy/presentation.scala	Fri Aug 19 14:53:38 2022 +0200
@@ -183,9 +183,9 @@
         deps.sessions_structure.build_requirements(presentation_sessions).flatMap(session =>
           using(open_session(session)) { session_context =>
             session_context.theory_names().flatMap { theory =>
-              session_context.theory(theory).files() match {
-                case None => Nil
-                case Some((thy, blobs)) =>
+              session_context.theory(theory).files0(permissive = true) match {
+                case Nil => Nil
+                case thy :: blobs =>
                   val thy_file_info = File_Info(theory, is_theory = true)
                   (thy -> thy_file_info) :: blobs.map(_ -> File_Info(theory))
               }