restrict to proper_session_theories;
authorwenzelm
Fri, 06 Jan 2023 14:37:55 +0100
changeset 76929 c7a165287df5
parent 76928 cd8f6634db17
child 76930 9ce0aa145d21
restrict to proper_session_theories;
src/Pure/Tools/update.scala
--- a/src/Pure/Tools/update.scala	Fri Jan 06 13:09:08 2023 +0100
+++ b/src/Pure/Tools/update.scala	Fri Jan 06 14:37:55 2023 +0100
@@ -84,11 +84,13 @@
         if build_results(session).ok && !exclude(session)
       } {
         progress.echo("Session " + session + " ...")
+        val proper_session_theory =
+          build_results.deps(session).proper_session_theories.map(_.theory).toSet
         using(database_context.open_session0(session)) { session_context =>
           for {
             db <- session_context.session_db()
             theory <- store.read_theories(db, session)
-            if !seen_theory(theory)
+            if proper_session_theory(theory) && !seen_theory(theory)
           } {
             seen_theory += theory
             val theory_context = session_context.theory(theory)