src/Pure/Thy/sessions.scala
changeset 65471 05e5bffcf1d8
parent 65468 c41791ad75c3
child 65475 4519c8cc4bec
     1.1 --- a/src/Pure/Thy/sessions.scala	Wed Apr 12 21:13:43 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Wed Apr 12 22:32:55 2017 +0200
     1.3 @@ -85,7 +85,7 @@
     1.4  
     1.5    sealed case class Base(
     1.6      global_theories: Map[String, String] = Map.empty,
     1.7 -    loaded_theories: Map[String, Document.Node.Name] = Map.empty,
     1.8 +    loaded_theories: Map[String, String] = Map.empty,
     1.9      known_theories: Map[String, Document.Node.Name] = Map.empty,
    1.10      known_theories_local: Map[String, Document.Node.Name] = Map.empty,
    1.11      known_files: Map[JFile, List[Document.Node.Name]] = Map.empty,
    1.12 @@ -96,8 +96,6 @@
    1.13    {
    1.14      def platform_path: Base =
    1.15        copy(
    1.16 -        loaded_theories =
    1.17 -          for ((a, b) <- loaded_theories) yield (a, b.map(File.platform_path(_))),
    1.18          known_theories =
    1.19            for ((a, b) <- known_theories) yield (a, b.map(File.platform_path(_))),
    1.20          known_theories_local =
    1.21 @@ -108,10 +106,6 @@
    1.22      def loaded_theory(name: Document.Node.Name): Boolean =
    1.23        loaded_theories.isDefinedAt(name.theory)
    1.24  
    1.25 -    def dest_loaded_theories: List[(String, String)] =
    1.26 -      for ((theory, node_name) <- loaded_theories.toList)
    1.27 -        yield (theory, node_name.node)
    1.28 -
    1.29      def dest_known_theories: List[(String, String)] =
    1.30        for ((theory, node_name) <- known_theories.toList)
    1.31          yield (theory, node_name.node)