--- 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)