# HG changeset patch
# User wenzelm
# Date 1521214083 -3600
# Node ID e4903b803b8b4cd1e170e67770216ae9bbda9d0f
# Parent  15027fb50a0cde2622468a2f688277c22b97f04e
clarified signature;

diff -r 15027fb50a0c -r e4903b803b8b src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Fri Mar 16 15:43:56 2018 +0100
+++ b/src/Pure/Thy/thy_resources.scala	Fri Mar 16 16:28:03 2018 +0100
@@ -50,6 +50,13 @@
     }
   }
 
+  sealed case class Theories_Result(
+    val requirements: List[Document.Node.Name],
+    val version: Document.Version,
+    val state: Document.State)
+  {
+  }
+
   class Session private[Thy_Resources](
     session_options: Options,
     override val resources: Thy_Resources) extends isabelle.Session(session_options, resources)
@@ -59,24 +66,19 @@
     def use_theories(
       theories: List[(String, Position.T)],
       qualifier: String = Sessions.DRAFT,
-      master_dir: String = ""): (List[Document.Node.Name], Document.State) =
+      master_dir: String = ""): Theories_Result =
     {
       val requirements =
         resources.load_theories(session, theories, qualifier = qualifier, master_dir = master_dir)
-      val state = consolidated_state(requirements)
-      (requirements, state)
-    }
 
-    def consolidated_state(requirements: List[Document.Node.Name]): Document.State =
-    {
-      val promise = Future.promise[Document.State]
+      val result = Future.promise[Theories_Result]
 
       def check_state
       {
         val state = session.current_state()
         state.stable_tip_version match {
           case Some(version) if requirements.forall(state.node_consolidated(version, _)) =>
-            try { promise.fulfill(state) }
+            try { result.fulfill(Theories_Result(requirements, version, state)) }
             catch { case _: IllegalStateException => }
           case _ =>
         }
@@ -89,9 +91,9 @@
 
       session.commands_changed += consumer
       check_state
-      val state = promise.join
+      result.join
       session.commands_changed -= consumer
-      state
+      result.join
     }
   }