more interruptible use_theories;
authorwenzelm
Sat Mar 17 17:23:35 2018 +0100 (14 months ago)
changeset 6789225e2b621bdcb
parent 67891 4f383cd54f69
child 67893 c854e50c2114
more interruptible use_theories;
tuned comments;
src/Pure/Thy/thy_resources.scala
     1.1 --- a/src/Pure/Thy/thy_resources.scala	Sat Mar 17 17:13:27 2018 +0100
     1.2 +++ b/src/Pure/Thy/thy_resources.scala	Sat Mar 17 17:23:35 2018 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4  /*  Title:      Pure/Thy/thy_resources.scala
     1.5      Author:     Makarius
     1.6  
     1.7 -PIDE resources for theory files.
     1.8 +PIDE resources for theory files: load/unload theories via PIDE document updates.
     1.9  */
    1.10  
    1.11  package isabelle
    1.12 @@ -77,6 +77,10 @@
    1.13  
    1.14        val result = Future.promise[Theories_Result]
    1.15  
    1.16 +      val check_progress =
    1.17 +        Event_Timer.request(Time.now(), repeat = Some(Time.seconds(0.5)))
    1.18 +          { if (progress.stopped) result.cancel }
    1.19 +
    1.20        def check_state
    1.21        {
    1.22          val state = session.current_state()
    1.23 @@ -96,13 +100,17 @@
    1.24            case changed => if (dep_theories.exists(changed.nodes)) check_state
    1.25          }
    1.26  
    1.27 -      session.commands_changed += consumer
    1.28 -      check_state
    1.29 -      result.join
    1.30 -      session.commands_changed -= consumer
    1.31 +      try {
    1.32 +        session.commands_changed += consumer
    1.33 +        check_state
    1.34 +        result.join_result
    1.35 +        session.commands_changed -= consumer
    1.36 +      }
    1.37 +      finally {
    1.38 +        resources.unload_theories(session, id, dep_theories)
    1.39 +      }
    1.40  
    1.41 -      resources.unload_theories(session, id, dep_theories)
    1.42 -
    1.43 +      check_progress.cancel
    1.44        result.join
    1.45      }
    1.46    }