avoid result based on outdated state, e.g. relevant for use_theories with changed files;
authorwenzelm
Mon, 17 Oct 2022 14:11:59 +0200
changeset 76323 3637a0d06fe1
parent 76322 43e66527fa93
child 76324 6108b1751c1b
avoid result based on outdated state, e.g. relevant for use_theories with changed files;
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))
       }
     }