more strict AFP properties;
authorwenzelm
Mon, 25 Mar 2019 17:21:26 +0100
changeset 69981 3dced198b9ec
parent 69980 f2e3adfd916f
child 69982 f150253cb201
more strict AFP properties;
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")
   }
 }