more robust check_state loop, even without session activity (e.g. idempotent use_theories);
authorwenzelm
Sat Mar 17 18:30:13 2018 +0100 (14 months ago)
changeset 67894fee080c4045f
parent 67893 c854e50c2114
child 67895 cd00999d2d30
more robust check_state loop, even without session activity (e.g. idempotent use_theories);
src/Pure/Thy/thy_resources.scala
     1.1 --- a/src/Pure/Thy/thy_resources.scala	Sat Mar 17 18:18:53 2018 +0100
     1.2 +++ b/src/Pure/Thy/thy_resources.scala	Sat Mar 17 18:30:13 2018 +0100
     1.3 @@ -77,10 +77,6 @@
     1.4  
     1.5        val result = Future.promise[Theories_Result]
     1.6  
     1.7 -      val check_progress =
     1.8 -        Event_Timer.request(Time.now(), repeat = Some(Time.seconds(0.5)))
     1.9 -          { if (progress.stopped) result.cancel }
    1.10 -
    1.11        def check_state
    1.12        {
    1.13          val state = session.current_state()
    1.14 @@ -95,6 +91,10 @@
    1.15          }
    1.16        }
    1.17  
    1.18 +      val check_progress =
    1.19 +        Event_Timer.request(Time.now(), repeat = Some(Time.seconds(0.5)))
    1.20 +          { if (progress.stopped) result.cancel else check_state }
    1.21 +
    1.22        val consumer =
    1.23          Session.Consumer[Session.Commands_Changed](getClass.getName) {
    1.24            case changed => if (dep_theories.exists(changed.nodes)) check_state
    1.25 @@ -102,15 +102,14 @@
    1.26  
    1.27        try {
    1.28          session.commands_changed += consumer
    1.29 -        check_state
    1.30          result.join_result
    1.31 +        check_progress.cancel
    1.32          session.commands_changed -= consumer
    1.33        }
    1.34        finally {
    1.35          resources.unload_theories(session, id, dep_theories)
    1.36        }
    1.37  
    1.38 -      check_progress.cancel
    1.39        result.join
    1.40      }
    1.41    }