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