# HG changeset patch
# User wenzelm
# Date 1553526688 -3600
# Node ID 4744e75393d97db0e507fe63eebbd9dc2f20feef
# Parent  4ecdd3eaec046b78aac41a237ecbdf683376a40c
clarified signature;

diff -r 4ecdd3eaec04 -r 4744e75393d9 src/Pure/Admin/afp.scala
--- a/src/Pure/Admin/afp.scala	Mon Mar 25 15:48:08 2019 +0100
+++ b/src/Pure/Admin/afp.scala	Mon Mar 25 16:11:28 2019 +0100
@@ -107,7 +107,7 @@
   }
 
 
-  /* entries and sessions */
+  /* entries */
 
   val entries_map: SortedMap[String, AFP.Entry] =
   {
@@ -133,6 +133,14 @@
   }
 
   val entries: List[AFP.Entry] = entries_map.toList.map(_._2)
+
+
+  /* sessions */
+
+  val sessions_map: SortedMap[String, AFP.Entry] =
+    (SortedMap.empty[String, AFP.Entry] /: entries)(
+      { case (m1, e) => (m1 /: e.sessions)({ case (m2, s) => m2 + (s -> e) }) })
+
   val sessions: List[String] = entries.flatMap(_.sessions)
 
   val sessions_structure: Sessions.Structure =