--- a/src/Pure/PIDE/document.scala Sat Dec 31 12:35:00 2022 +0100
+++ b/src/Pure/PIDE/document.scala Sat Dec 31 12:38:48 2022 +0100
@@ -94,10 +94,10 @@
def apply(node: String, master_dir: String = "", theory: String = ""): Name =
new Name(node, master_dir, theory)
- val empty: Name = Name("")
+ def loaded_theory(theory: String): Document.Node.Name =
+ Name(theory, theory = theory)
- def loaded_theory(theory: String): Document.Node.Name =
- Document.Node.Name(theory, theory = theory)
+ val empty: Name = Name("")
object Ordering extends scala.math.Ordering[Name] {
def compare(name1: Name, name2: Name): Int = name1.node compare name2.node