src/Pure/Thy/sessions.scala
changeset 65499 fc7f03cbccbc
parent 65498 2af863e28204
child 65500 a6644e0e8728
     1.1 --- a/src/Pure/Thy/sessions.scala	Mon Apr 17 20:54:48 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Mon Apr 17 21:00:38 2017 +0200
     1.3 @@ -33,8 +33,7 @@
     1.4        def bases_iterator(local: Boolean) =
     1.5          for {
     1.6            base <- bases.iterator
     1.7 -          known = base.known
     1.8 -          (_, name) <- (if (local) known.known_theories_local else known.known_theories).iterator
     1.9 +          (_, name) <- (if (local) base.known.theories_local else base.known.theories).iterator
    1.10          } yield name
    1.11  
    1.12        def local_theories_iterator =
    1.13 @@ -74,18 +73,14 @@
    1.14    }
    1.15  
    1.16    sealed case class Known(
    1.17 -    known_theories: Map[String, Document.Node.Name] = Map.empty,
    1.18 -    known_theories_local: Map[String, Document.Node.Name] = Map.empty,
    1.19 -    known_files: Map[JFile, List[Document.Node.Name]] = Map.empty)
    1.20 +    theories: Map[String, Document.Node.Name] = Map.empty,
    1.21 +    theories_local: Map[String, Document.Node.Name] = Map.empty,
    1.22 +    files: Map[JFile, List[Document.Node.Name]] = Map.empty)
    1.23    {
    1.24      def platform_path: Known =
    1.25 -      copy(
    1.26 -        known_theories =
    1.27 -          for ((a, b) <- known_theories) yield (a, b.map(File.platform_path(_))),
    1.28 -        known_theories_local =
    1.29 -          for ((a, b) <- known_theories_local) yield (a, b.map(File.platform_path(_))),
    1.30 -        known_files =
    1.31 -          for ((a, b) <- known_files) yield (a, b.map(c => c.map(File.platform_path(_)))))
    1.32 +      copy(theories = for ((a, b) <- theories) yield (a, b.map(File.platform_path(_))),
    1.33 +        theories_local = for ((a, b) <- theories_local) yield (a, b.map(File.platform_path(_))),
    1.34 +        files = for ((a, b) <- files) yield (a, b.map(c => c.map(File.platform_path(_)))))
    1.35    }
    1.36  
    1.37    object Base
    1.38 @@ -114,13 +109,13 @@
    1.39        loaded_theories.isDefinedAt(name.theory)
    1.40  
    1.41      def known_theory(name: String): Option[Document.Node.Name] =
    1.42 -      known.known_theories.get(name)
    1.43 +      known.theories.get(name)
    1.44  
    1.45      def known_file(file: JFile): Option[Document.Node.Name] =
    1.46 -      known.known_files.getOrElse(file, Nil).headOption
    1.47 +      known.files.getOrElse(file, Nil).headOption
    1.48  
    1.49      def dest_known_theories: List[(String, String)] =
    1.50 -      for ((theory, node_name) <- known.known_theories.toList)
    1.51 +      for ((theory, node_name) <- known.theories.toList)
    1.52          yield (theory, node_name.node)
    1.53    }
    1.54