# HG changeset patch
# User wenzelm
# Date 1491487299 -7200
# Node ID ad9e2c1665b670707ad5afa85b61d85296ed9bff
# Parent  c728f922f6578bc4718f0c8f6793d2207b330adb
tuned signature;

diff -r c728f922f657 -r ad9e2c1665b6 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Thu Apr 06 15:57:33 2017 +0200
+++ b/src/Pure/PIDE/document.scala	Thu Apr 06 16:01:39 2017 +0200
@@ -98,7 +98,6 @@
     object Name
     {
       val empty = Name("")
-      def theory(theory: String): Name = Name(theory, "", theory)
 
       object Ordering extends scala.math.Ordering[Name]
       {
@@ -115,7 +114,9 @@
           case _ => false
         }
 
+      def loaded_theory: Name = Name(theory, "", theory)
       def is_theory: Boolean = theory.nonEmpty
+
       override def toString: String = if (is_theory) theory else node
 
       def map(f: String => String): Name = copy(f(node), f(master_dir), theory)
diff -r c728f922f657 -r ad9e2c1665b6 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Thu Apr 06 15:57:33 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Thu Apr 06 16:01:39 2017 +0200
@@ -76,7 +76,7 @@
 
     session_base.known_theories.get(theory) orElse session_base.known_theories.get(theory0) match
     {
-      case Some(name) if session_base.loaded_theory(name) => Document.Node.Name.theory(name.theory)
+      case Some(name) if session_base.loaded_theory(name) => name.loaded_theory
       case Some(name) => name
       case None =>
         val path = Path.explode(s)