provide maintainers as seen in AFP/admin;
authorwenzelm
Mon, 25 Mar 2019 14:47:54 +0100
changeset 69976 98a440cfbb2b
parent 69975 35cc58a54ffc
child 69977 3c166df11085
provide maintainers as seen in AFP/admin; suppress empty properties;
src/Pure/Admin/afp.scala
--- a/src/Pure/Admin/afp.scala	Mon Mar 25 14:40:28 2019 +0100
+++ b/src/Pure/Admin/afp.scala	Mon Mar 25 14:47:54 2019 +0100
@@ -28,6 +28,11 @@
   /* entries */
 
   sealed case class Entry(name: String, metadata: Properties.T, sessions: List[String])
+  {
+    def maintainers: List[String] =
+      Library.space_explode(',', Properties.get(metadata, "notify").getOrElse("")).
+        map(_.trim).filter(_.nonEmpty)
+  }
 }
 
 class AFP private(options: Options, val base_dir: Path)
@@ -68,7 +73,8 @@
         case Section(name) => flush(); section = name
         case Property(a, b) =>
           if (section == "") err("Property without a section")
-          props = (a -> b.trim) :: props
+          val c = b.trim
+          if (c.nonEmpty) props = (a -> c) :: props
         case Extra_Line(line) =>
           props match {
             case Nil => err("Extra line without a property")