tuned signature;
authorwenzelm
Thu, 06 Apr 2017 16:01:39 +0200
changeset 65409 ad9e2c1665b6
parent 65408 c728f922f657
child 65410 44253ed65acd
tuned signature;
src/Pure/PIDE/document.scala
src/Pure/PIDE/resources.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)
--- 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)