record status of already committed nodes;
authorwenzelm
Fri Sep 07 17:05:02 2018 +0200 (9 months ago)
changeset 6892576ce16eefab9
parent 68924 feed46aa1969
child 68926 5129fcc1b6c0
record status of already committed nodes;
tuned signature;
src/Pure/Thy/thy_resources.scala
     1.1 --- a/src/Pure/Thy/thy_resources.scala	Fri Sep 07 17:03:58 2018 +0200
     1.2 +++ b/src/Pure/Thy/thy_resources.scala	Fri Sep 07 17:05:02 2018 +0200
     1.3 @@ -66,11 +66,14 @@
     1.4    class Theories_Result private[Thy_Resources](
     1.5      val state: Document.State,
     1.6      val version: Document.Version,
     1.7 -    val nodes: List[(Document.Node.Name, Document_Status.Node_Status)])
     1.8 +    val nodes: List[(Document.Node.Name, Document_Status.Node_Status)],
     1.9 +    val nodes_committed: List[(Document.Node.Name, Document_Status.Node_Status)])
    1.10    {
    1.11 -    def node_names: List[Document.Node.Name] = nodes.map(_._1)
    1.12 -    def ok: Boolean = nodes.forall({ case (_, st) => st.ok })
    1.13 -    def snapshot(name: Document.Node.Name): Document.Snapshot = stable_snapshot(state, version, name)
    1.14 +    def snapshot(name: Document.Node.Name): Document.Snapshot =
    1.15 +      stable_snapshot(state, version, name)
    1.16 +
    1.17 +    def ok: Boolean =
    1.18 +      (nodes.iterator ++ nodes_committed.iterator).forall({ case (_, st) => st.ok })
    1.19    }
    1.20  
    1.21    val default_check_delay: Double = 0.5
    1.22 @@ -108,7 +111,7 @@
    1.23        last_update: Time = Time.now(),
    1.24        nodes_status: Document_Status.Nodes_Status = Document_Status.Nodes_Status.empty,
    1.25        already_initialized: Set[Document.Node.Name] = Set.empty,
    1.26 -      already_committed: Set[Document.Node.Name] = Set.empty,
    1.27 +      already_committed: Map[Document.Node.Name, Document_Status.Node_Status] = Map.empty,
    1.28        result: Promise[Theories_Result] = Future.promise[Theories_Result])
    1.29      {
    1.30        def update(new_nodes_status: Document_Status.Nodes_Status): Use_Theories_State =
    1.31 @@ -137,7 +140,7 @@
    1.32        def check_result(
    1.33            state: Document.State,
    1.34            version: Document.Version,
    1.35 -          theories: List[Document.Node.Name],
    1.36 +          dep_theories: List[Document.Node.Name],
    1.37            beyond_limit: Boolean,
    1.38            watchdog_timeout: Time,
    1.39            commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit])
    1.40 @@ -147,29 +150,35 @@
    1.41            if (commit.isDefined) {
    1.42              val committed =
    1.43                for {
    1.44 -                name <- theories
    1.45 -                if !already_committed(name) && state.node_consolidated(version, name)
    1.46 +                name <- dep_theories
    1.47 +                if !already_committed.isDefinedAt(name) && state.node_consolidated(version, name)
    1.48                }
    1.49                yield {
    1.50                  val snapshot = stable_snapshot(state, version, name)
    1.51                  val status = Document_Status.Node_Status.make(state, version, name)
    1.52                  commit.get.apply(snapshot, status)
    1.53 -                name
    1.54 +                (name -> status)
    1.55                }
    1.56              copy(already_committed = already_committed ++ committed)
    1.57            }
    1.58            else this
    1.59  
    1.60          if (beyond_limit || watchdog(watchdog_timeout) ||
    1.61 -          theories.forall(name =>
    1.62 -            already_committed(name) ||
    1.63 +          dep_theories.forall(name =>
    1.64 +            already_committed.isDefinedAt(name) ||
    1.65              state.node_consolidated(version, name) ||
    1.66              nodes_status.quasi_consolidated(name)))
    1.67          {
    1.68            val nodes =
    1.69 -            for (name <- theories)
    1.70 +            for (name <- dep_theories)
    1.71              yield { (name -> Document_Status.Node_Status.make(state, version, name)) }
    1.72 -          try { result.fulfill(new Theories_Result(state, version, nodes)) }
    1.73 +          val nodes_committed =
    1.74 +            for {
    1.75 +              name <- dep_theories
    1.76 +              status <- already_committed.get(name)
    1.77 +            } yield (name -> status)
    1.78 +
    1.79 +          try { result.fulfill(new Theories_Result(state, version, nodes, nodes_committed)) }
    1.80            catch { case _: IllegalStateException => }
    1.81          }
    1.82