ensure foundational order of commits, taking Pure as implicit starting point;
authorwenzelm
Sat Sep 08 16:52:38 2018 +0200 (8 months ago)
changeset 68949e848328cb2c1
parent 68948 9abd946f990c
child 68950 53f7b6b9f734
ensure foundational order of commits, taking Pure as implicit starting point;
src/Pure/Thy/thy_resources.scala
     1.1 --- a/src/Pure/Thy/thy_resources.scala	Sat Sep 08 14:30:31 2018 +0200
     1.2 +++ b/src/Pure/Thy/thy_resources.scala	Sat Sep 08 16:52:38 2018 +0200
     1.3 @@ -153,18 +153,23 @@
     1.4        {
     1.5          val st1 =
     1.6            if (commit.isDefined) {
     1.7 -            val committed =
     1.8 -              for {
     1.9 -                name <- dep_theories
    1.10 -                if !already_committed.isDefinedAt(name) && state.node_consolidated(version, name)
    1.11 -              }
    1.12 -              yield {
    1.13 -                val snapshot = stable_snapshot(state, version, name)
    1.14 -                val status = Document_Status.Node_Status.make(state, version, name)
    1.15 -                commit.get.apply(snapshot, status)
    1.16 -                (name -> status)
    1.17 -              }
    1.18 -            copy(already_committed = already_committed ++ committed)
    1.19 +            val already_committed1 =
    1.20 +              (already_committed /: dep_theories)({ case (committed, name) =>
    1.21 +                def parents_committed: Boolean =
    1.22 +                  version.nodes(name).header.imports.forall({ case (parent, _) =>
    1.23 +                    Sessions.is_pure(parent.theory) || committed.isDefinedAt(parent)
    1.24 +                  })
    1.25 +                if (!committed.isDefinedAt(name) && parents_committed &&
    1.26 +                    state.node_consolidated(version, name))
    1.27 +                {
    1.28 +                  val snapshot = stable_snapshot(state, version, name)
    1.29 +                  val status = Document_Status.Node_Status.make(state, version, name)
    1.30 +                  commit.get.apply(snapshot, status)
    1.31 +                  committed + (name -> status)
    1.32 +                }
    1.33 +                else committed
    1.34 +              })
    1.35 +            copy(already_committed = already_committed1)
    1.36            }
    1.37            else this
    1.38