src/Pure/PIDE/document.scala

--- a/src/Pure/PIDE/document.scala	Tue May 29 18:09:08 2018 +0200
+++ b/src/Pure/PIDE/document.scala	Tue May 29 20:00:10 2018 +0200
@@ -383,6 +383,8 @@
       new Nodes(graph3.map_node(name, _ => node))
     }
 
+    def domain: Set[Node.Name] = graph.domain
+
     def iterator: Iterator[(Node.Name, Node)] =
       graph.iterator.map({ case (name, (node, _)) => (name, node) })