tuned;
authorwenzelm
Sat Mar 17 16:24:59 2018 +0100 (14 months ago)
changeset 678895c438b774b4d
parent 67888 3bf62a6e50e7
child 67890 f4a505d6bc94
tuned;
src/Pure/Thy/thy_resources.scala
     1.1 --- a/src/Pure/Thy/thy_resources.scala	Sat Mar 17 16:18:05 2018 +0100
     1.2 +++ b/src/Pure/Thy/thy_resources.scala	Sat Mar 17 16:24:59 2018 +0100
     1.3 @@ -51,9 +51,9 @@
     1.4    }
     1.5  
     1.6    sealed case class Theories_Result(
     1.7 -    val nodes: List[(Document.Node.Name, Protocol.Node_Status)],
     1.8      val state: Document.State,
     1.9 -    val version: Document.Version)
    1.10 +    val version: Document.Version,
    1.11 +    val nodes: List[(Document.Node.Name, Protocol.Node_Status)])
    1.12    {
    1.13      def ok: Boolean = nodes.forall({ case (_, st) => st.ok })
    1.14    }
    1.15 @@ -82,10 +82,10 @@
    1.16          val state = session.current_state()
    1.17          state.stable_tip_version match {
    1.18            case Some(version) if dep_theories.forall(state.node_consolidated(version, _)) =>
    1.19 -            def status(name: Document.Node.Name): Protocol.Node_Status =
    1.20 -              Protocol.node_status(state, version, name, version.nodes(name))
    1.21 -            val nodes = for (name <- dep_theories) yield (name -> status(name))
    1.22 -            try { result.fulfill(Theories_Result(nodes, state, version)) }
    1.23 +            val nodes =
    1.24 +              for (name <- dep_theories)
    1.25 +              yield (name -> Protocol.node_status(state, version, name, version.nodes(name)))
    1.26 +            try { result.fulfill(Theories_Result(state, version, nodes)) }
    1.27              catch { case _: IllegalStateException => }
    1.28            case _ =>
    1.29          }