tuned signature;
authorwenzelm
Mon Mar 25 14:32:33 2019 +0100 (4 weeks ago)
changeset 69974916726680a66
parent 69973 a3e3be17dca5
child 69975 35cc58a54ffc
tuned signature;
src/Pure/Admin/afp.scala
     1.1 --- a/src/Pure/Admin/afp.scala	Mon Mar 25 14:19:26 2019 +0100
     1.2 +++ b/src/Pure/Admin/afp.scala	Mon Mar 25 14:32:33 2019 +0100
     1.3 @@ -7,6 +7,9 @@
     1.4  package isabelle
     1.5  
     1.6  
     1.7 +import scala.collection.immutable.SortedMap
     1.8 +
     1.9 +
    1.10  object AFP
    1.11  {
    1.12    val repos_source = "https://isabelle.sketis.net/repos/afp-devel"
    1.13 @@ -90,29 +93,34 @@
    1.14    val main_dir: Path = base_dir + Path.explode("thys")
    1.15  
    1.16  
    1.17 -  /* entries with metadata and sessions */
    1.18 +  /* entries and sessions */
    1.19  
    1.20 -  val entries: List[AFP.Entry] =
    1.21 +  val entries_map: SortedMap[String, AFP.Entry] =
    1.22    {
    1.23      val entry_metadata = AFP.Metadata.read(base_dir + Path.explode("metadata/metadata"))
    1.24  
    1.25      val entries =
    1.26 -      (for (name <- Sessions.parse_roots(main_dir + Sessions.ROOTS)) yield {
    1.27 +      for (name <- Sessions.parse_roots(main_dir + Sessions.ROOTS)) yield {
    1.28          val metadata =
    1.29            entry_metadata.getOrElse(name, error("Entry without metadata: " + quote(name)))
    1.30          val sessions =
    1.31            Sessions.parse_root_entries(main_dir + Path.explode(name) + Sessions.ROOT).map(_.name)
    1.32          AFP.Entry(name, metadata, sessions)
    1.33 -      }).sortBy(_.name)
    1.34 +      }
    1.35  
    1.36 -    val entry_set = entries.iterator.map(_.name).toSet
    1.37 +    val entries_map =
    1.38 +      (SortedMap.empty[String, AFP.Entry] /: entries)({ case (m, e) => m + (e.name -> e) })
    1.39 +
    1.40      val extra_metadata =
    1.41 -      (for ((name, _) <- entry_metadata.iterator if !entry_set(name)) yield name).toList.sorted
    1.42 -    if (extra_metadata.nonEmpty) error("Meta data without entry: " + commas_quote(extra_metadata))
    1.43 +      (for ((name, _) <- entry_metadata.iterator if !entries_map.isDefinedAt(name)) yield name).
    1.44 +        toList.sorted
    1.45 +    if (extra_metadata.nonEmpty)
    1.46 +      error("Meta data without entry: " + commas_quote(extra_metadata))
    1.47  
    1.48 -    entries
    1.49 +    entries_map
    1.50    }
    1.51  
    1.52 +  val entries: List[AFP.Entry] = entries_map.toList.map(_._2)
    1.53    val sessions: List[String] = entries.flatMap(_.sessions)
    1.54  
    1.55    val sessions_structure: Sessions.Structure =