src/Pure/Thy/thy_resources.scala
changeset 68883 3653b3ad729e
parent 68771 7e1978b9a4d1
child 68884 9b97d0b20d95
     1.1 --- a/src/Pure/Thy/thy_resources.scala	Sun Sep 02 20:51:07 2018 +0200
     1.2 +++ b/src/Pure/Thy/thy_resources.scala	Sun Sep 02 21:22:52 2018 +0200
     1.3 @@ -111,6 +111,8 @@
     1.4            master_dir = proper_string(master_dir) getOrElse tmp_dir_name, progress = progress)
     1.5        val dep_theories_set = dep_theories.toSet
     1.6  
     1.7 +      val nodes_status_update = Synchronized(Document_Status.Nodes_Status.empty_update)
     1.8 +
     1.9        val result = Future.promise[Theories_Result]
    1.10  
    1.11        def check_state(beyond_limit: Boolean = false)
    1.12 @@ -118,7 +120,11 @@
    1.13          val state = session.current_state()
    1.14          state.stable_tip_version match {
    1.15            case Some(version) =>
    1.16 -            if (beyond_limit || dep_theories.forall(state.node_consolidated(version, _))) {
    1.17 +            if (beyond_limit ||
    1.18 +                dep_theories.forall(name =>
    1.19 +                  state.node_consolidated(version, name) ||
    1.20 +                  nodes_status_update.value._1.is_terminated(name)))
    1.21 +            {
    1.22                val nodes =
    1.23                  for (name <- dep_theories)
    1.24                  yield (name -> Document_Status.Node_Status.make(state, version, name))
    1.25 @@ -144,8 +150,6 @@
    1.26  
    1.27        val theories_progress = Synchronized(Set.empty[Document.Node.Name])
    1.28  
    1.29 -      val nodes_status_update = Synchronized(Document_Status.Nodes_Status.empty_update)
    1.30 -
    1.31        val delay_nodes_status =
    1.32          Standard_Thread.delay_first(nodes_status_delay max Time.zero) {
    1.33            val (nodes_status, names) = nodes_status_update.value
    1.34 @@ -160,19 +164,19 @@
    1.35                val state = snapshot.state
    1.36                val version = snapshot.version
    1.37  
    1.38 -              if (nodes_status_delay >= Time.zero) {
    1.39 -                nodes_status_update.change(
    1.40 -                  { case upd @ (nodes_status, _) =>
    1.41 -                      val domain =
    1.42 -                        if (nodes_status.is_empty) dep_theories_set
    1.43 -                        else changed.nodes.iterator.filter(dep_theories_set).toSet
    1.44 -                      val upd1 =
    1.45 -                        nodes_status.update(resources.session_base, state, version,
    1.46 -                          domain = Some(domain), trim = changed.assignment).getOrElse(upd)
    1.47 -                      if (upd == upd1) upd
    1.48 -                      else { delay_nodes_status.invoke; upd1 }
    1.49 -                  })
    1.50 -              }
    1.51 +              nodes_status_update.change(
    1.52 +                { case upd @ (nodes_status, _) =>
    1.53 +                    val domain =
    1.54 +                      if (nodes_status.is_empty) dep_theories_set
    1.55 +                      else changed.nodes.iterator.filter(dep_theories_set).toSet
    1.56 +                    val upd1 =
    1.57 +                      nodes_status.update(resources.session_base, state, version,
    1.58 +                        domain = Some(domain), trim = changed.assignment).getOrElse(upd)
    1.59 +                    if (nodes_status_delay >= Time.zero && upd != upd1)
    1.60 +                      delay_nodes_status.invoke
    1.61 +
    1.62 +                    upd1
    1.63 +                })
    1.64  
    1.65                val check_theories =
    1.66                  (for {