# HG changeset patch
# User wenzelm
# Date 1672485934 -3600
# Node ID 81848d12aba313858da0d789ac5f38972260881f
# Parent  ef1f7d56f7c8acfd2ee2035053f84d6fbb5badcf
clarified modules;

diff -r ef1f7d56f7c8 -r 81848d12aba3 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sat Dec 31 12:16:22 2022 +0100
+++ b/src/Pure/PIDE/document.scala	Sat Dec 31 12:25:34 2022 +0100
@@ -96,6 +96,9 @@
 
       val empty: Name = Name("")
 
+      def loaded_theory(theory: String): Document.Node.Name =
+        Document.Node.Name(theory, theory = theory)
+
       object Ordering extends scala.math.Ordering[Name] {
         def compare(name1: Name, name2: Name): Int = name1.node compare name2.node
       }
diff -r ef1f7d56f7c8 -r 81848d12aba3 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Sat Dec 31 12:16:22 2022 +0100
+++ b/src/Pure/PIDE/resources.scala	Sat Dec 31 12:25:34 2022 +0100
@@ -81,9 +81,6 @@
     Document.Node.Name(node, master_dir = master_dir, theory = theory)
   }
 
-  def loaded_theory_node(theory: String): Document.Node.Name =
-    Document.Node.Name(theory, theory = theory)
-
 
   /* source files of Isabelle/ML bootstrap */
 
@@ -175,12 +172,12 @@
     if (literal_import && !Url.is_base_name(s)) {
       error("Bad import of theory from other session via file-path: " + quote(s))
     }
-    if (session_base.loaded_theory(theory)) loaded_theory_node(theory)
+    if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory)
     else {
       find_theory_node(theory) match {
         case Some(node_name) => node_name
         case None =>
-          if (Url.is_base_name(s) && literal_theory(s)) loaded_theory_node(theory)
+          if (Url.is_base_name(s) && literal_theory(s)) Document.Node.Name.loaded_theory(theory)
           else file_node(Path.explode(s).thy, dir = dir, theory = theory)
       }
     }
diff -r ef1f7d56f7c8 -r 81848d12aba3 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Sat Dec 31 12:16:22 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Sat Dec 31 12:25:34 2022 +0100
@@ -93,7 +93,7 @@
     find_theory(file) getOrElse {
       val node = file.getPath
       val theory = theory_name(Sessions.DRAFT, Thy_Header.theory_name(node))
-      if (session_base.loaded_theory(theory)) loaded_theory_node(theory)
+      if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory)
       else {
         val master_dir = file.getParent
         Document.Node.Name(node, master_dir = master_dir, theory = theory)
diff -r ef1f7d56f7c8 -r 81848d12aba3 src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Sat Dec 31 12:16:22 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Sat Dec 31 12:25:34 2022 +0100
@@ -35,7 +35,7 @@
       val vfs = VFSManager.getVFSForPath(path)
       val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
       val theory = theory_name(Sessions.DRAFT, Thy_Header.theory_name(node))
-      if (session_base.loaded_theory(theory)) loaded_theory_node(theory)
+      if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory)
       else {
         val master_dir = vfs.getParentOfPath(path)
         Document.Node.Name(node, master_dir = master_dir, theory = theory)