# HG changeset patch
# User wenzelm
# Date 1660472286 -7200
# Node ID c32ecc4b4720ae38bfa4e270ee0be6f515564473
# Parent  2b2c09f4e7b5fde651475a2b1d394b5863537ca5
clarified theory_names with exported content;

diff -r 2b2c09f4e7b5 -r c32ecc4b4720 src/Pure/Thy/export_theory.scala
--- 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)