synchronous use_theories, based on consolidated_state;
authorwenzelm
Sun Nov 12 21:32:33 2017 +0100 (13 months ago)
changeset 67064fb487246ef4f
parent 67063 10d608cc7470
child 67065 d9a347af82ab
synchronous use_theories, based on consolidated_state;
src/Pure/Thy/thy_resources.scala
     1.1 --- a/src/Pure/Thy/thy_resources.scala	Sun Nov 12 20:50:24 2017 +0100
     1.2 +++ b/src/Pure/Thy/thy_resources.scala	Sun Nov 12 21:32:33 2017 +0100
     1.3 @@ -49,14 +49,48 @@
     1.4    }
     1.5  
     1.6    class Session private[Thy_Resources](
     1.7 -    options: Options, override val resources: Thy_Resources)
     1.8 -    extends isabelle.Session(options, resources)
     1.9 +    session_options: Options,
    1.10 +    override val resources: Thy_Resources) extends isabelle.Session(session_options, resources)
    1.11    {
    1.12      session =>
    1.13  
    1.14 -    def load_theories(theories: List[(String, Position.T)],
    1.15 -        qualifier: String = Sessions.DRAFT, master_dir: String = ""): List[Document.Node.Name] =
    1.16 -      resources.load_theories(session, theories, qualifier = qualifier, master_dir = master_dir)
    1.17 +    def use_theories(
    1.18 +      theories: List[(String, Position.T)],
    1.19 +      qualifier: String = Sessions.DRAFT,
    1.20 +      master_dir: String = ""): (List[Document.Node.Name], Document.State) =
    1.21 +    {
    1.22 +      val requirements =
    1.23 +        resources.load_theories(session, theories, qualifier = qualifier, master_dir = master_dir)
    1.24 +      val state = consolidated_state(requirements)
    1.25 +      (requirements, state)
    1.26 +    }
    1.27 +
    1.28 +    def consolidated_state(requirements: List[Document.Node.Name]): Document.State =
    1.29 +    {
    1.30 +      val promise = Future.promise[Document.State]
    1.31 +
    1.32 +      def check_state
    1.33 +      {
    1.34 +        val state = session.current_state()
    1.35 +        state.stable_tip_version match {
    1.36 +          case Some(version) if requirements.forall(state.node_consolidated(version, _)) =>
    1.37 +            try { promise.fulfill(state) }
    1.38 +            catch { case _: IllegalStateException => }
    1.39 +          case _ =>
    1.40 +        }
    1.41 +      }
    1.42 +
    1.43 +      val consumer =
    1.44 +        Session.Consumer[Session.Commands_Changed](getClass.getName) {
    1.45 +          case changed => if (requirements.exists(changed.nodes)) check_state
    1.46 +        }
    1.47 +
    1.48 +      session.commands_changed += consumer
    1.49 +      check_state
    1.50 +      val state = promise.join
    1.51 +      session.commands_changed -= consumer
    1.52 +      state
    1.53 +    }
    1.54    }
    1.55  
    1.56