# HG changeset patch
# User wenzelm
# Date 1672486728 -3600
# Node ID 4d19dc723a6dfc92e2da477648c5fd4911cfc0ba
# Parent  252ed80e1a567a7ce88f0b68b692cceae3537f50
tuned;

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