clarified signature;
authorwenzelm
Mon, 25 Mar 2019 16:11:28 +0100
changeset 70161 4744e75393d9
parent 70160 4ecdd3eaec04
child 70162 f2e3adfd916f
clarified signature;
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 =