--- a/src/Pure/Thy/export_theory.scala Sun Aug 14 12:01:47 2022 +0200
+++ b/src/Pure/Thy/export_theory.scala Sun Aug 14 12:18:06 2022 +0200
@@ -29,7 +29,7 @@
progress: Progress = new Progress
): Session = {
val thys =
- for (theory <- session_context.theory_names()) yield {
+ for (theory <- theory_names(session_context)) yield {
progress.echo("Reading theory " + theory)
read_theory(session_context.theory(theory))
}
@@ -104,6 +104,12 @@
theory_context.get(Export.THEORY_PREFIX + "parents")
.map(entry => Library.trim_split_lines(entry.uncompressed.text))
+ def theory_names(session_context: Export.Session_Context): List[String] =
+ for {
+ theory <- session_context.theory_names()
+ if read_theory_parents(session_context.theory(theory)).isDefined
+ } yield theory
+
def no_theory: Theory =
Theory("", Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Map.empty)