diff -r 634768c0bd22 -r 2a1583baaaa0 src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Wed Sep 05 20:29:23 2018 +0200
+++ b/src/Pure/Thy/thy_resources.scala	Wed Sep 05 21:56:44 2018 +0200
@@ -55,6 +55,14 @@
     }
   }
 
+  private def stable_snapshot(
+    state: Document.State, version: Document.Version, name: Document.Node.Name): Document.Snapshot =
+  {
+    val snapshot = state.snapshot(name)
+    assert(version.id == snapshot.version.id)
+    snapshot
+  }
+
   class Theories_Result private[Thy_Resources](
     val state: Document.State,
     val version: Document.Version,
@@ -62,13 +70,7 @@
   {
     def node_names: List[Document.Node.Name] = nodes.map(_._1)
     def ok: Boolean = nodes.forall({ case (_, st) => st.ok })
-
-    def snapshot(node_name: Document.Node.Name): Document.Snapshot =
-    {
-      val snapshot = state.snapshot(node_name)
-      assert(version.id == snapshot.version.id)
-      snapshot
-    }
+    def snapshot(name: Document.Node.Name): Document.Snapshot = stable_snapshot(state, version, name)
   }
 
   val default_check_delay: Double = 0.5
@@ -99,7 +101,9 @@
     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)
+      already_initialized: Set[Document.Node.Name] = Set.empty,
+      already_committed: Set[Document.Node.Name] = Set.empty,
+      result: Promise[Theories_Result] = Future.promise[Theories_Result])
     {
       def update(new_nodes_status: Document_Status.Nodes_Status): Use_Theories_State =
         copy(last_update = Time.now(), nodes_status = new_nodes_status)
@@ -110,16 +114,61 @@
       def initialized_theories(
         state: Document.State,
         version: Document.Version,
-        new_theories: List[Document.Node.Name]): (List[Document.Node.Name], Use_Theories_State) =
+        theories: List[Document.Node.Name]): (List[Document.Node.Name], Use_Theories_State) =
       {
         val initialized =
           for {
-            name <- new_theories
+            name <- theories
             if !already_initialized(name) &&
               Document_Status.Node_Status.make(state, version, name).initialized
           } yield name
         (initialized, copy(already_initialized = already_initialized ++ initialized))
       }
+
+      def cancel_result { result.cancel }
+      def await_result { result.join_result }
+      def join_result: Theories_Result = result.join
+      def check_result(
+          state: Document.State,
+          version: Document.Version,
+          theories: List[Document.Node.Name],
+          beyond_limit: Boolean,
+          watchdog_timeout: Time,
+          commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit])
+        : Use_Theories_State =
+      {
+        val st1 =
+          if (commit.isDefined) {
+            val committed =
+              for {
+                name <- theories
+                if !already_committed(name) && state.node_consolidated(version, name)
+              }
+              yield {
+                val snapshot = stable_snapshot(state, version, name)
+                val status = Document_Status.Node_Status.make(state, version, name)
+                commit.get.apply(snapshot, status)
+                name
+              }
+            copy(already_committed = already_committed ++ committed)
+          }
+          else this
+
+        if (beyond_limit || watchdog(watchdog_timeout) ||
+          theories.forall(name =>
+            already_committed(name) ||
+            state.node_consolidated(version, name) ||
+            nodes_status.quasi_consolidated(name)))
+        {
+          val nodes =
+            for (name <- theories)
+            yield { (name -> Document_Status.Node_Status.make(state, version, name)) }
+          try { result.fulfill(new Theories_Result(state, version, nodes)) }
+          catch { case _: IllegalStateException => }
+        }
+
+        st1
+      }
     }
 
     def use_theories(
@@ -131,6 +180,8 @@
       watchdog_timeout: Time = Time.zero,
       nodes_status_delay: Time = Time.seconds(default_nodes_status_delay),
       id: UUID = UUID(),
+      // commit: must not block, must not fail
+      commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit] = None,
       progress: Progress = No_Progress): Theories_Result =
     {
       val dep_theories =
@@ -143,25 +194,14 @@
       val dep_theories_set = dep_theories.toSet
 
       val use_theories_state = Synchronized(Use_Theories_State())
-      val result = Future.promise[Theories_Result]
 
-      def check_state(beyond_limit: Boolean = false)
+      def check_result(beyond_limit: Boolean = false)
       {
         val state = session.current_state()
         state.stable_tip_version match {
           case Some(version) =>
-            val st = use_theories_state.value
-            if (beyond_limit || st.watchdog(watchdog_timeout) ||
-                dep_theories.forall(name =>
-                  state.node_consolidated(version, name) ||
-                  st.nodes_status.quasi_consolidated(name)))
-            {
-              val nodes =
-                for (name <- dep_theories)
-                yield (name -> Document_Status.Node_Status.make(state, version, name))
-              try { result.fulfill(new Theories_Result(state, version, nodes)) }
-              catch { case _: IllegalStateException => }
-            }
+            use_theories_state.change(
+              _.check_result(state, version, dep_theories, beyond_limit, watchdog_timeout, commit))
           case None =>
         }
       }
@@ -171,10 +211,10 @@
         var check_count = 0
         Event_Timer.request(Time.now(), repeat = Some(check_delay))
           {
-            if (progress.stopped) result.cancel
+            if (progress.stopped) use_theories_state.value.cancel_result
             else {
               check_count += 1
-              check_state(check_limit > 0 && check_count > check_limit)
+              check_result(check_limit > 0 && check_count > check_limit)
             }
           }
       }
@@ -235,7 +275,7 @@
               for ((theory, percentage) <- theory_percentages)
                 progress.theory_percentage("", theory, percentage)
 
-              check_state()
+              check_result()
             }
         }
       }
@@ -243,7 +283,7 @@
       try {
         session.commands_changed += consumer
         resources.load_theories(session, id, dep_theories, progress)
-        result.join_result
+        use_theories_state.value.await_result
         check_progress.cancel
       }
       finally {
@@ -251,7 +291,7 @@
         resources.unload_theories(session, id, dep_theories)
       }
 
-      result.join
+      use_theories_state.value.join_result
     }
 
     def purge_theories(