src/Pure/Thy/sessions.scala
changeset 65498 2af863e28204
parent 65496 ca8dcb2a500c
child 65499 fc7f03cbccbc
     1.1 --- a/src/Pure/Thy/sessions.scala	Mon Apr 17 20:33:18 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Mon Apr 17 20:54:48 2017 +0200
     1.3 @@ -33,7 +33,8 @@
     1.4        def bases_iterator(local: Boolean) =
     1.5          for {
     1.6            base <- bases.iterator
     1.7 -          (_, name) <- (if (local) base.known_theories_local else base.known_theories).iterator
     1.8 +          known = base.known
     1.9 +          (_, name) <- (if (local) known.known_theories_local else known.known_theories).iterator
    1.10          } yield name
    1.11  
    1.12        def local_theories_iterator =
    1.13 @@ -112,12 +113,14 @@
    1.14      def loaded_theory(name: Document.Node.Name): Boolean =
    1.15        loaded_theories.isDefinedAt(name.theory)
    1.16  
    1.17 -    def known_theories: Map[String, Document.Node.Name] = known.known_theories
    1.18 -    def known_theories_local: Map[String, Document.Node.Name] = known.known_theories_local
    1.19 -    def known_files: Map[JFile, List[Document.Node.Name]] = known.known_files
    1.20 +    def known_theory(name: String): Option[Document.Node.Name] =
    1.21 +      known.known_theories.get(name)
    1.22 +
    1.23 +    def known_file(file: JFile): Option[Document.Node.Name] =
    1.24 +      known.known_files.getOrElse(file, Nil).headOption
    1.25  
    1.26      def dest_known_theories: List[(String, String)] =
    1.27 -      for ((theory, node_name) <- known_theories.toList)
    1.28 +      for ((theory, node_name) <- known.known_theories.toList)
    1.29          yield (theory, node_name.node)
    1.30    }
    1.31