diff -r 100f018096c8 -r bf7336731981 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Tue May 29 20:03:24 2018 +0200 +++ b/src/Pure/PIDE/document.scala Tue May 29 22:25:59 2018 +0200 @@ -921,6 +921,13 @@ } } + def node_initialized(version: Version, name: Node.Name): Boolean = + name.is_theory && + (version.nodes(name).commands.iterator.find(_.potentially_initialized) match { + case None => false + case Some(command) => command_states(version, command).headOption.exists(_.initialized) + }) + def node_consolidated(version: Version, name: Node.Name): Boolean = !name.is_theory || version.nodes(name).commands.reverse.iterator.