# HG changeset patch
# User wenzelm
# Date 1492455638 -7200
# Node ID fc7f03cbccbcbb213ff8ccb521d0b3528c4b08cd
# Parent  2af863e28204cab2eb6aa98fb189fc3e7a79bf57
tuned signature;

diff -r 2af863e28204 -r fc7f03cbccbc src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Apr 17 20:54:48 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon Apr 17 21:00:38 2017 +0200
@@ -33,8 +33,7 @@
       def bases_iterator(local: Boolean) =
         for {
           base <- bases.iterator
-          known = base.known
-          (_, name) <- (if (local) known.known_theories_local else known.known_theories).iterator
+          (_, name) <- (if (local) base.known.theories_local else base.known.theories).iterator
         } yield name
 
       def local_theories_iterator =
@@ -74,18 +73,14 @@
   }
 
   sealed case class Known(
-    known_theories: Map[String, Document.Node.Name] = Map.empty,
-    known_theories_local: Map[String, Document.Node.Name] = Map.empty,
-    known_files: Map[JFile, List[Document.Node.Name]] = Map.empty)
+    theories: Map[String, Document.Node.Name] = Map.empty,
+    theories_local: Map[String, Document.Node.Name] = Map.empty,
+    files: Map[JFile, List[Document.Node.Name]] = Map.empty)
   {
     def platform_path: Known =
-      copy(
-        known_theories =
-          for ((a, b) <- known_theories) yield (a, b.map(File.platform_path(_))),
-        known_theories_local =
-          for ((a, b) <- known_theories_local) yield (a, b.map(File.platform_path(_))),
-        known_files =
-          for ((a, b) <- known_files) yield (a, b.map(c => c.map(File.platform_path(_)))))
+      copy(theories = for ((a, b) <- theories) yield (a, b.map(File.platform_path(_))),
+        theories_local = for ((a, b) <- theories_local) yield (a, b.map(File.platform_path(_))),
+        files = for ((a, b) <- files) yield (a, b.map(c => c.map(File.platform_path(_)))))
   }
 
   object Base
@@ -114,13 +109,13 @@
       loaded_theories.isDefinedAt(name.theory)
 
     def known_theory(name: String): Option[Document.Node.Name] =
-      known.known_theories.get(name)
+      known.theories.get(name)
 
     def known_file(file: JFile): Option[Document.Node.Name] =
-      known.known_files.getOrElse(file, Nil).headOption
+      known.files.getOrElse(file, Nil).headOption
 
     def dest_known_theories: List[(String, String)] =
-      for ((theory, node_name) <- known.known_theories.toList)
+      for ((theory, node_name) <- known.theories.toList)
         yield (theory, node_name.node)
   }