--- a/src/Pure/PIDE/document_status.scala Sun Sep 02 20:51:07 2018 +0200
+++ b/src/Pure/PIDE/document_status.scala Sun Sep 02 21:22:52 2018 +0200
@@ -192,6 +192,12 @@
def apply(name: Document.Node.Name): Node_Status = rep(name)
def get(name: Document.Node.Name): Option[Node_Status] = rep.get(name)
+ def is_terminated(name: Document.Node.Name): Boolean =
+ rep.get(name) match {
+ case Some(st) => st.terminated
+ case None => false
+ }
+
def overall_node_status(name: Document.Node.Name): Overall_Node_Status.Value =
rep.get(name) match {
case Some(st) if st.consolidated =>