# HG changeset patch
# User wenzelm
# Date 1568662230 -7200
# Node ID a8afe8eb3529cfce4c3ac8cc50438450d2f312f8
# Parent  fb94d68314fad042bdb9ed0f1d0a1521097a25c5
tuned signature;

diff -r fb94d68314fa -r a8afe8eb3529 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Mon Sep 16 20:06:25 2019 +0200
+++ b/src/Pure/PIDE/document.scala	Mon Sep 16 21:30:30 2019 +0200
@@ -102,8 +102,6 @@
     {
       val empty = Name("")
 
-      def loaded_theory(theory: String): Name = Name(theory, "", theory)
-
       object Ordering extends scala.math.Ordering[Name]
       {
         def compare(name1: Name, name2: Name): Int = name1.node compare name2.node
diff -r fb94d68314fa -r a8afe8eb3529 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Mon Sep 16 20:06:25 2019 +0200
+++ b/src/Pure/PIDE/resources.scala	Mon Sep 16 21:30:30 2019 +0200
@@ -55,6 +55,9 @@
     Document.Node.Name(node, master_dir, theory)
   }
 
+  def loaded_theory_node(theory: String): Document.Node.Name =
+    Document.Node.Name(theory, "", theory)
+
 
   /* source files of Isabelle/ML bootstrap */
 
@@ -133,13 +136,13 @@
   def import_name(qualifier: String, dir: String, s: String): Document.Node.Name =
   {
     val theory = theory_name(qualifier, Thy_Header.import_name(s))
-    if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory)
+    if (session_base.loaded_theory(theory)) loaded_theory_node(theory)
     else {
       find_theory_node(theory) match {
         case Some(node_name) => node_name
         case None =>
           if (Thy_Header.is_base_name(s) && Long_Name.is_qualified(s))
-            Document.Node.Name.loaded_theory(theory)
+            loaded_theory_node(theory)
           else make_theory_node(dir, thy_path(Path.explode(s)), theory)
       }
     }
diff -r fb94d68314fa -r a8afe8eb3529 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Mon Sep 16 20:06:25 2019 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Mon Sep 16 21:30:30 2019 +0200
@@ -97,7 +97,7 @@
     find_theory(Sessions.DRAFT, file) getOrElse {
       val node = file.getPath
       val theory = theory_name(Sessions.DRAFT, Thy_Header.theory_name(node))
-      if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory)
+      if (session_base.loaded_theory(theory)) loaded_theory_node(theory)
       else {
         val master_dir = file.getParent
         Document.Node.Name(node, master_dir, theory)
diff -r fb94d68314fa -r a8afe8eb3529 src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Mon Sep 16 20:06:25 2019 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Mon Sep 16 21:30:30 2019 +0200
@@ -41,7 +41,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)) Document.Node.Name.loaded_theory(theory)
+      if (session_base.loaded_theory(theory)) loaded_theory_node(theory)
       else {
         val master_dir = vfs.getParentOfPath(path)
         Document.Node.Name(node, master_dir, theory)