diff -r 55b12fde48d0 -r 51bd9e9501fb src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Wed Sep 05 09:36:17 2018 +0200
+++ b/src/Pure/Thy/thy_resources.scala	Wed Sep 05 20:00:38 2018 +0200
@@ -96,6 +96,32 @@
 
     /* theories */
 
+    private sealed case class Use_Theories_State(
+      last_update: Time = Time.now(),
+      nodes_status: Document_Status.Nodes_Status = Document_Status.Nodes_Status.empty,
+      already_initialized: Set[Document.Node.Name] = Set.empty)
+    {
+      def update(new_nodes_status: Document_Status.Nodes_Status): Use_Theories_State =
+        copy(last_update = Time.now(), nodes_status = new_nodes_status)
+
+      def watchdog(watchdog_timeout: Time): Boolean =
+        watchdog_timeout > Time.zero && Time.now() - last_update > watchdog_timeout
+
+      def initialized_theories(
+        state: Document.State,
+        version: Document.Version,
+        new_theories: List[Document.Node.Name]): (List[Document.Node.Name], Use_Theories_State) =
+      {
+        val initialized =
+          for {
+            name <- new_theories
+            if !already_initialized(name) &&
+              Document_Status.Node_Status.make(state, version, name).initialized
+          } yield name
+        (initialized, copy(already_initialized = already_initialized ++ initialized))
+      }
+    }
+
     def use_theories(
       theories: List[String],
       qualifier: String = Sessions.DRAFT,
@@ -116,23 +142,19 @@
       }
       val dep_theories_set = dep_theories.toSet
 
-      val current_nodes_status = Synchronized(Document_Status.Nodes_Status.empty)
-
+      val use_theories_state = Synchronized(Use_Theories_State())
       val result = Future.promise[Theories_Result]
 
-      var watchdog_time = Synchronized(Time.now())
-      def watchdog: Boolean =
-        watchdog_timeout > Time.zero && Time.now() - watchdog_time.value > watchdog_timeout
-
       def check_state(beyond_limit: Boolean = false)
       {
         val state = session.current_state()
         state.stable_tip_version match {
           case Some(version) =>
-            if (beyond_limit || watchdog ||
+            val st = use_theories_state.value
+            if (beyond_limit || st.watchdog(watchdog_timeout) ||
                 dep_theories.forall(name =>
                   state.node_consolidated(version, name) ||
-                  current_nodes_status.value.quasi_consolidated(name)))
+                  st.nodes_status.quasi_consolidated(name)))
             {
               val nodes =
                 for (name <- dep_theories)
@@ -159,11 +181,9 @@
 
       val consumer =
       {
-        val theories_progress = Synchronized(Set.empty[Document.Node.Name])
-
         val delay_nodes_status =
           Standard_Thread.delay_first(nodes_status_delay max Time.zero) {
-            progress.nodes_status(current_nodes_status.value)
+            progress.nodes_status(use_theories_state.value.nodes_status)
           }
 
         Session.Consumer[Session.Commands_Changed](getClass.getName) {
@@ -173,17 +193,15 @@
               val state = snapshot.state
               val version = snapshot.version
 
-              watchdog_time.change(_ => Time.now())
-
               val theory_percentages =
-                current_nodes_status.change_result(nodes_status =>
+                use_theories_state.change_result(st =>
                   {
                     val domain =
-                      if (nodes_status.is_empty) dep_theories_set
+                      if (st.nodes_status.is_empty) dep_theories_set
                       else changed.nodes.iterator.filter(dep_theories_set).toSet
 
                     val (nodes_status_changed, nodes_status1) =
-                      nodes_status.update(resources.session_base, state, version,
+                      st.nodes_status.update(resources.session_base, state, version,
                         domain = Some(domain), trim = changed.assignment)
 
                     if (nodes_status_delay >= Time.zero && nodes_status_changed) {
@@ -195,27 +213,22 @@
                         (name, node_status) <- nodes_status1.present.iterator
                         if changed.nodes.contains(name)
                         p1 = node_status.percentage
-                        if p1 > 0 && Some(p1) != nodes_status.get(name).map(_.percentage)
+                        if p1 > 0 && Some(p1) != st.nodes_status.get(name).map(_.percentage)
                       } yield (name.theory, p1)).toList
 
-                    (progress_percentage, nodes_status1)
+                    (progress_percentage, st.update(nodes_status1))
                   })
 
               val check_theories =
                 (for {
                   command <- changed.commands.iterator
                   if dep_theories_set(command.node_name) && command.potentially_initialized
-                } yield command.node_name).toSet
+                } yield command.node_name).toList
 
               if (check_theories.nonEmpty) {
                 val initialized =
-                  theories_progress.change_result(theories =>
-                  {
-                    val initialized =
-                      (check_theories -- theories).toList.filter(name =>
-                        Document_Status.Node_Status.make(state, version, name).initialized)
-                    (initialized, theories ++ initialized)
-                  })
+                  use_theories_state.change_result(
+                    _.initialized_theories(state, version, check_theories))
                 initialized.map(_.theory).sorted.foreach(progress.theory("", _))
               }