tuned signature;
authorwenzelm
Thu Apr 06 16:01:39 2017 +0200 (2017-04-06)
changeset 65409ad9e2c1665b6
parent 65408 c728f922f657
child 65410 44253ed65acd
tuned signature;
src/Pure/PIDE/document.scala
src/Pure/PIDE/resources.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Thu Apr 06 15:57:33 2017 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Thu Apr 06 16:01:39 2017 +0200
     1.3 @@ -98,7 +98,6 @@
     1.4      object Name
     1.5      {
     1.6        val empty = Name("")
     1.7 -      def theory(theory: String): Name = Name(theory, "", theory)
     1.8  
     1.9        object Ordering extends scala.math.Ordering[Name]
    1.10        {
    1.11 @@ -115,7 +114,9 @@
    1.12            case _ => false
    1.13          }
    1.14  
    1.15 +      def loaded_theory: Name = Name(theory, "", theory)
    1.16        def is_theory: Boolean = theory.nonEmpty
    1.17 +
    1.18        override def toString: String = if (is_theory) theory else node
    1.19  
    1.20        def map(f: String => String): Name = copy(f(node), f(master_dir), theory)
     2.1 --- a/src/Pure/PIDE/resources.scala	Thu Apr 06 15:57:33 2017 +0200
     2.2 +++ b/src/Pure/PIDE/resources.scala	Thu Apr 06 16:01:39 2017 +0200
     2.3 @@ -76,7 +76,7 @@
     2.4  
     2.5      session_base.known_theories.get(theory) orElse session_base.known_theories.get(theory0) match
     2.6      {
     2.7 -      case Some(name) if session_base.loaded_theory(name) => Document.Node.Name.theory(name.theory)
     2.8 +      case Some(name) if session_base.loaded_theory(name) => name.loaded_theory
     2.9        case Some(name) => name
    2.10        case None =>
    2.11          val path = Path.explode(s)