# HG changeset patch
# User wenzelm
# Date 1665918178 -7200
# Node ID fab6568b119d49c2976bf36cc70f0ace845ecc17
# Parent  c5c747ce46d298a9cfc3dc79f098396b14c53ded
more robust: active consumer for check_state/check_progress;

diff -r c5c747ce46d2 -r fab6568b119d src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Sat Oct 15 16:09:05 2022 +0200
+++ b/src/Pure/PIDE/headless.scala	Sun Oct 16 13:02:58 2022 +0200
@@ -289,7 +289,7 @@
         } resources.load_theories(session, id, load_theories, dep_files, unicode_symbols, progress)
       }
 
-      val check_progress = {
+      lazy val check_progress = {
         var check_count = 0
         Event_Timer.request(Time.now(), repeat = Some(check_delay)) {
           if (progress.stopped) use_theories_state.change(_.cancel_result)
@@ -363,7 +363,7 @@
 
       try {
         session.commands_changed += consumer
-        check_state()
+        check_progress
         use_theories_state.guarded_access(_.join_result)
         check_progress.cancel()
       }