# HG changeset patch
# User wenzelm
# Date 1553530886 -3600
# Node ID 3dced198b9ec44da5084352b90d5c6cc6a1373c3
# Parent  f2e3adfd916f2736c45ed50555c1195561451dc1
more strict AFP properties;

diff -r f2e3adfd916f -r 3dced198b9ec src/Pure/Admin/afp.scala
--- a/src/Pure/Admin/afp.scala	Mon Mar 25 16:45:08 2019 +0100
+++ b/src/Pure/Admin/afp.scala	Mon Mar 25 17:21:26 2019 +0100
@@ -43,12 +43,13 @@
 
     def title: String = get_string("title")
     def authors: List[String] = get_strings("author")
-    def date: Option[Date] = get("date").map(parse_date(_))
+    def date: Date =
+      parse_date(get("date").getOrElse(error("Missing date for entry " + quote(name))))
     def topics: List[String] = get_strings("topic")
-    def `abstract`: String = get_string("abstract")
+    def `abstract`: String = get_string("abstract").trim
     def maintainers: List[String] = get_strings("notify")
     def contributors: List[String] = get_strings("contributors")
-    def license: Option[String] = get("license")
+    def license: String = get("license").getOrElse("BSD")
   }
 }