# HG changeset patch
# User wenzelm
# Date 1536418358 -7200
# Node ID e848328cb2c11c19211669944e29611efdc89074
# Parent  9abd946f990cb81281d808d524ed89a0c00ac4e4
ensure foundational order of commits, taking Pure as implicit starting point;

diff -r 9abd946f990c -r e848328cb2c1 src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Sat Sep 08 14:30:31 2018 +0200
+++ b/src/Pure/Thy/thy_resources.scala	Sat Sep 08 16:52:38 2018 +0200
@@ -153,18 +153,23 @@
       {
         val st1 =
           if (commit.isDefined) {
-            val committed =
-              for {
-                name <- dep_theories
-                if !already_committed.isDefinedAt(name) && state.node_consolidated(version, name)
-              }
-              yield {
-                val snapshot = stable_snapshot(state, version, name)
-                val status = Document_Status.Node_Status.make(state, version, name)
-                commit.get.apply(snapshot, status)
-                (name -> status)
-              }
-            copy(already_committed = already_committed ++ committed)
+            val already_committed1 =
+              (already_committed /: dep_theories)({ case (committed, name) =>
+                def parents_committed: Boolean =
+                  version.nodes(name).header.imports.forall({ case (parent, _) =>
+                    Sessions.is_pure(parent.theory) || committed.isDefinedAt(parent)
+                  })
+                if (!committed.isDefinedAt(name) && parents_committed &&
+                    state.node_consolidated(version, name))
+                {
+                  val snapshot = stable_snapshot(state, version, name)
+                  val status = Document_Status.Node_Status.make(state, version, name)
+                  commit.get.apply(snapshot, status)
+                  committed + (name -> status)
+                }
+                else committed
+              })
+            copy(already_committed = already_committed1)
           }
           else this