--- 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
}