# HG changeset patch
# User wenzelm
# Date 1521300299 -3600
# Node ID 5c438b774b4d69fb1f5172082595375ad1513e6c
# Parent  3bf62a6e50e748b4858437275daeb241dd85a3da
tuned;

diff -r 3bf62a6e50e7 -r 5c438b774b4d src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Sat Mar 17 16:18:05 2018 +0100
+++ b/src/Pure/Thy/thy_resources.scala	Sat Mar 17 16:24:59 2018 +0100
@@ -51,9 +51,9 @@
   }
 
   sealed case class Theories_Result(
-    val nodes: List[(Document.Node.Name, Protocol.Node_Status)],
     val state: Document.State,
-    val version: Document.Version)
+    val version: Document.Version,
+    val nodes: List[(Document.Node.Name, Protocol.Node_Status)])
   {
     def ok: Boolean = nodes.forall({ case (_, st) => st.ok })
   }
@@ -82,10 +82,10 @@
         val state = session.current_state()
         state.stable_tip_version match {
           case Some(version) if dep_theories.forall(state.node_consolidated(version, _)) =>
-            def status(name: Document.Node.Name): Protocol.Node_Status =
-              Protocol.node_status(state, version, name, version.nodes(name))
-            val nodes = for (name <- dep_theories) yield (name -> status(name))
-            try { result.fulfill(Theories_Result(nodes, state, version)) }
+            val nodes =
+              for (name <- dep_theories)
+              yield (name -> Protocol.node_status(state, version, name, version.nodes(name)))
+            try { result.fulfill(Theories_Result(state, version, nodes)) }
             catch { case _: IllegalStateException => }
           case _ =>
         }