diff -r a4d265a6c5cc -r 3047b7671279 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue Sep 03 14:58:29 2019 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Sep 03 15:24:04 2019 +0200
@@ -76,6 +76,11 @@
   type Edit_Text = Edit[Text.Edit, Text.Perspective]
   type Edit_Command = Edit[Command.Edit, Command.Perspective]
 
+  def theory_graph[A](
+      entries: List[((Node.Name, A), List[Node.Name])],
+      permissive: Boolean = false): Graph[Node.Name, A] =
+    Graph.make(entries, symmetric = true, permissive = permissive)(Node.Name.Theory_Ordering)
+
   object Node
   {
     /* header and name */