diff -r 39c90514faf8 -r a56eab490f4e src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sat Aug 31 21:34:39 2019 +0200
+++ b/src/Pure/PIDE/document.scala	Sun Sep 01 22:57:25 2019 +0200
@@ -106,6 +106,11 @@
       {
         def compare(name1: Name, name2: Name): Int = name1.node compare name2.node
       }
+
+      object Theory_Ordering extends scala.math.Ordering[Name]
+      {
+        def compare(name1: Name, name2: Name): Int = name1.theory compare name2.theory
+      }
     }
 
     sealed case class Name(node: String, master_dir: String = "", theory: String = "")
@@ -136,6 +141,8 @@
     {
       def map(f: String => String): Entry = copy(name = name.map(f))
 
+      def imports: List[Node.Name] = header.imports.map(_._1)
+
       override def toString: String = name.toString
     }