# HG changeset patch
# User wenzelm
# Date 1553524736 -3600
# Node ID 3c166df110851ddb48efe0cd53afc25e1b46edec
# Parent  98a440cfbb2b47b7e88276ab0cce7e36d1edb76a
clarified signature: explicitly typed interfaces;

diff -r 98a440cfbb2b -r 3c166df11085 src/Pure/Admin/afp.scala
--- a/src/Pure/Admin/afp.scala	Mon Mar 25 14:47:54 2019 +0100
+++ b/src/Pure/Admin/afp.scala	Mon Mar 25 15:38:56 2019 +0100
@@ -7,6 +7,7 @@
 package isabelle
 
 
+import java.time.{LocalDate, ZoneId}
 import scala.collection.immutable.SortedMap
 
 
@@ -27,11 +28,28 @@
 
   /* entries */
 
+  def parse_date(s: String): Date =
+  {
+    val t = Date.Formatter.pattern("uuuu-MM-dd").parse(s)
+    val zone_id = ZoneId.of("Europe/Berlin")
+    Date(LocalDate.from(t).atStartOfDay(zone_id))
+  }
+
   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)
+    def get(prop: String): Option[String] = Properties.get(metadata, prop)
+    def get_string(prop: String): String = get(prop).getOrElse("")
+    def get_strings(prop: String): List[String] =
+      Library.space_explode(',', get_string(prop)).map(_.trim).filter(_.nonEmpty)
+
+    def title: String = get_string("title")
+    def authors: List[String] = get_strings("author")
+    def date: Option[Date] = get("date").map(parse_date(_))
+    def topics: List[String] = get_strings("topic")
+    def `abstract`: String = get_string("abstract")
+    def maintainers: List[String] = get_strings("notify")
+    def contributors: List[String] = get_strings("contributors")
+    def license: Option[String] = get("license")
   }
 }