# HG changeset patch
# User wenzelm
# Date 1666008719 -7200
# Node ID 3637a0d06fe194ba932032b06e45c63f817e4b3b
# Parent  43e66527fa93e78e5d275f46505605b8e0bd2600
avoid result based on outdated state, e.g. relevant for use_theories with changed files;

diff -r 43e66527fa93 -r 3637a0d06fe1 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Mon Oct 17 12:15:23 2022 +0200
+++ b/src/Pure/PIDE/headless.scala	Mon Oct 17 14:11:59 2022 +0200
@@ -239,9 +239,14 @@
         def committed(name: Document.Node.Name): Boolean =
           loaded_theory(name) || st1.already_committed.isDefinedAt(name)
 
+        val (load_theories0, load_state1) =
+          load_state.next(dep_graph, consolidated(state, version, _))
+
+        val load_theories = load_theories0.filterNot(committed)
+
         val result1 = {
           val stopped = beyond_limit || watchdog
-          if (!finished_result &&
+          if (!finished_result && load_theories.isEmpty &&
               (stopped || dep_graph.keys_iterator.forall(consolidated(state, version, _)))
           ) {
             @tailrec def make_nodes(
@@ -272,10 +277,7 @@
           else result
         }
 
-        val (load_theories, load_state1) =
-          load_state.next(dep_graph, consolidated(state, version, _))
-
-        (load_theories.filterNot(committed), st1.copy(result = result1, load_state = load_state1))
+        (load_theories, st1.copy(result = result1, load_state = load_state1))
       }
     }