diff -r 252ed80e1a56 -r 4d19dc723a6d src/Pure/PIDE/document.scala --- 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