# HG changeset patch
# User wenzelm
# Date 1553520753 -3600
# Node ID 916726680a66255978779c603eb2f4dd2c5a9156
# Parent  a3e3be17dca56c2c304f5277ce4ed8e938b0d542
tuned signature;

diff -r a3e3be17dca5 -r 916726680a66 src/Pure/Admin/afp.scala
--- a/src/Pure/Admin/afp.scala	Mon Mar 25 14:19:26 2019 +0100
+++ b/src/Pure/Admin/afp.scala	Mon Mar 25 14:32:33 2019 +0100
@@ -7,6 +7,9 @@
 package isabelle
 
 
+import scala.collection.immutable.SortedMap
+
+
 object AFP
 {
   val repos_source = "https://isabelle.sketis.net/repos/afp-devel"
@@ -90,29 +93,34 @@
   val main_dir: Path = base_dir + Path.explode("thys")
 
 
-  /* entries with metadata and sessions */
+  /* entries and sessions */
 
-  val entries: List[AFP.Entry] =
+  val entries_map: SortedMap[String, AFP.Entry] =
   {
     val entry_metadata = AFP.Metadata.read(base_dir + Path.explode("metadata/metadata"))
 
     val entries =
-      (for (name <- Sessions.parse_roots(main_dir + Sessions.ROOTS)) yield {
+      for (name <- Sessions.parse_roots(main_dir + Sessions.ROOTS)) yield {
         val metadata =
           entry_metadata.getOrElse(name, error("Entry without metadata: " + quote(name)))
         val sessions =
           Sessions.parse_root_entries(main_dir + Path.explode(name) + Sessions.ROOT).map(_.name)
         AFP.Entry(name, metadata, sessions)
-      }).sortBy(_.name)
+      }
 
-    val entry_set = entries.iterator.map(_.name).toSet
+    val entries_map =
+      (SortedMap.empty[String, AFP.Entry] /: entries)({ case (m, e) => m + (e.name -> e) })
+
     val extra_metadata =
-      (for ((name, _) <- entry_metadata.iterator if !entry_set(name)) yield name).toList.sorted
-    if (extra_metadata.nonEmpty) error("Meta data without entry: " + commas_quote(extra_metadata))
+      (for ((name, _) <- entry_metadata.iterator if !entries_map.isDefinedAt(name)) yield name).
+        toList.sorted
+    if (extra_metadata.nonEmpty)
+      error("Meta data without entry: " + commas_quote(extra_metadata))
 
-    entries
+    entries_map
   }
 
+  val entries: List[AFP.Entry] = entries_map.toList.map(_._2)
   val sessions: List[String] = entries.flatMap(_.sessions)
 
   val sessions_structure: Sessions.Structure =