# HG changeset patch # User wenzelm # Date 1510518753 -3600 # Node ID fb487246ef4f016fec1861bb166d04dae18fafb4 # Parent 10d608cc7470216d58d012f57d78973df1911076 synchronous use_theories, based on consolidated_state; diff -r 10d608cc7470 -r fb487246ef4f src/Pure/Thy/thy_resources.scala --- a/src/Pure/Thy/thy_resources.scala Sun Nov 12 20:50:24 2017 +0100 +++ b/src/Pure/Thy/thy_resources.scala Sun Nov 12 21:32:33 2017 +0100 @@ -49,14 +49,48 @@ } class Session private[Thy_Resources]( - options: Options, override val resources: Thy_Resources) - extends isabelle.Session(options, resources) + session_options: Options, + override val resources: Thy_Resources) extends isabelle.Session(session_options, resources) { session => - def load_theories(theories: List[(String, Position.T)], - qualifier: String = Sessions.DRAFT, master_dir: String = ""): List[Document.Node.Name] = - resources.load_theories(session, theories, qualifier = qualifier, master_dir = master_dir) + def use_theories( + theories: List[(String, Position.T)], + qualifier: String = Sessions.DRAFT, + master_dir: String = ""): (List[Document.Node.Name], Document.State) = + { + val requirements = + resources.load_theories(session, theories, qualifier = qualifier, master_dir = master_dir) + val state = consolidated_state(requirements) + (requirements, state) + } + + def consolidated_state(requirements: List[Document.Node.Name]): Document.State = + { + val promise = Future.promise[Document.State] + + def check_state + { + val state = session.current_state() + state.stable_tip_version match { + case Some(version) if requirements.forall(state.node_consolidated(version, _)) => + try { promise.fulfill(state) } + catch { case _: IllegalStateException => } + case _ => + } + } + + val consumer = + Session.Consumer[Session.Commands_Changed](getClass.getName) { + case changed => if (requirements.exists(changed.nodes)) check_state + } + + session.commands_changed += consumer + check_state + val state = promise.join + session.commands_changed -= consumer + state + } }