--- 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 =