clarified theory_names with exported content;
authorwenzelm
Sun, 14 Aug 2022 12:18:06 +0200
changeset 75861 c32ecc4b4720
parent 75860 2b2c09f4e7b5
child 75862 186654cd2840
clarified theory_names with exported content;
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)