tuned signature;
authorwenzelm
Mon Apr 17 20:54:48 2017 +0200 (2017-04-17)
changeset 654982af863e28204
parent 65497 7966bd7c6461
child 65499 fc7f03cbccbc
tuned signature;
src/Pure/PIDE/resources.scala
src/Pure/Thy/sessions.scala
     1.1 --- a/src/Pure/PIDE/resources.scala	Mon Apr 17 20:33:18 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.scala	Mon Apr 17 20:54:48 2017 +0200
     1.3 @@ -83,7 +83,7 @@
     1.4      theory_name(qualifier, Thy_Header.import_name(s)) match {
     1.5        case (true, theory) => Document.Node.Name.loaded_theory(theory)
     1.6        case (false, theory) =>
     1.7 -        session_base.known_theories.get(theory) match {
     1.8 +        session_base.known_theory(theory) match {
     1.9            case Some(node_name) => node_name
    1.10            case None =>
    1.11              val path = Path.explode(s)
     2.1 --- a/src/Pure/Thy/sessions.scala	Mon Apr 17 20:33:18 2017 +0200
     2.2 +++ b/src/Pure/Thy/sessions.scala	Mon Apr 17 20:54:48 2017 +0200
     2.3 @@ -33,7 +33,8 @@
     2.4        def bases_iterator(local: Boolean) =
     2.5          for {
     2.6            base <- bases.iterator
     2.7 -          (_, name) <- (if (local) base.known_theories_local else base.known_theories).iterator
     2.8 +          known = base.known
     2.9 +          (_, name) <- (if (local) known.known_theories_local else known.known_theories).iterator
    2.10          } yield name
    2.11  
    2.12        def local_theories_iterator =
    2.13 @@ -112,12 +113,14 @@
    2.14      def loaded_theory(name: Document.Node.Name): Boolean =
    2.15        loaded_theories.isDefinedAt(name.theory)
    2.16  
    2.17 -    def known_theories: Map[String, Document.Node.Name] = known.known_theories
    2.18 -    def known_theories_local: Map[String, Document.Node.Name] = known.known_theories_local
    2.19 -    def known_files: Map[JFile, List[Document.Node.Name]] = known.known_files
    2.20 +    def known_theory(name: String): Option[Document.Node.Name] =
    2.21 +      known.known_theories.get(name)
    2.22 +
    2.23 +    def known_file(file: JFile): Option[Document.Node.Name] =
    2.24 +      known.known_files.getOrElse(file, Nil).headOption
    2.25  
    2.26      def dest_known_theories: List[(String, String)] =
    2.27 -      for ((theory, node_name) <- known_theories.toList)
    2.28 +      for ((theory, node_name) <- known.known_theories.toList)
    2.29          yield (theory, node_name.node)
    2.30    }
    2.31