# 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)) }