clarified signature;
authorwenzelm
Mon Mar 25 16:11:28 2019 +0100 (3 weeks ago)
changeset 699794744e75393d9
parent 69978 4ecdd3eaec04
child 69980 f2e3adfd916f
clarified signature;
src/Pure/Admin/afp.scala
     1.1 --- a/src/Pure/Admin/afp.scala	Mon Mar 25 15:48:08 2019 +0100
     1.2 +++ b/src/Pure/Admin/afp.scala	Mon Mar 25 16:11:28 2019 +0100
     1.3 @@ -107,7 +107,7 @@
     1.4    }
     1.5  
     1.6  
     1.7 -  /* entries and sessions */
     1.8 +  /* entries */
     1.9  
    1.10    val entries_map: SortedMap[String, AFP.Entry] =
    1.11    {
    1.12 @@ -133,6 +133,14 @@
    1.13    }
    1.14  
    1.15    val entries: List[AFP.Entry] = entries_map.toList.map(_._2)
    1.16 +
    1.17 +
    1.18 +  /* sessions */
    1.19 +
    1.20 +  val sessions_map: SortedMap[String, AFP.Entry] =
    1.21 +    (SortedMap.empty[String, AFP.Entry] /: entries)(
    1.22 +      { case (m1, e) => (m1 /: e.sessions)({ case (m2, s) => m2 + (s -> e) }) })
    1.23 +
    1.24    val sessions: List[String] = entries.flatMap(_.sessions)
    1.25  
    1.26    val sessions_structure: Sessions.Structure =