clarified signature: explicitly typed interfaces;
authorwenzelm
Mon Mar 25 15:38:56 2019 +0100 (3 weeks ago)
changeset 699773c166df11085
parent 69976 98a440cfbb2b
child 69978 4ecdd3eaec04
clarified signature: explicitly typed interfaces;
src/Pure/Admin/afp.scala
     1.1 --- a/src/Pure/Admin/afp.scala	Mon Mar 25 14:47:54 2019 +0100
     1.2 +++ b/src/Pure/Admin/afp.scala	Mon Mar 25 15:38:56 2019 +0100
     1.3 @@ -7,6 +7,7 @@
     1.4  package isabelle
     1.5  
     1.6  
     1.7 +import java.time.{LocalDate, ZoneId}
     1.8  import scala.collection.immutable.SortedMap
     1.9  
    1.10  
    1.11 @@ -27,11 +28,28 @@
    1.12  
    1.13    /* entries */
    1.14  
    1.15 +  def parse_date(s: String): Date =
    1.16 +  {
    1.17 +    val t = Date.Formatter.pattern("uuuu-MM-dd").parse(s)
    1.18 +    val zone_id = ZoneId.of("Europe/Berlin")
    1.19 +    Date(LocalDate.from(t).atStartOfDay(zone_id))
    1.20 +  }
    1.21 +
    1.22    sealed case class Entry(name: String, metadata: Properties.T, sessions: List[String])
    1.23    {
    1.24 -    def maintainers: List[String] =
    1.25 -      Library.space_explode(',', Properties.get(metadata, "notify").getOrElse("")).
    1.26 -        map(_.trim).filter(_.nonEmpty)
    1.27 +    def get(prop: String): Option[String] = Properties.get(metadata, prop)
    1.28 +    def get_string(prop: String): String = get(prop).getOrElse("")
    1.29 +    def get_strings(prop: String): List[String] =
    1.30 +      Library.space_explode(',', get_string(prop)).map(_.trim).filter(_.nonEmpty)
    1.31 +
    1.32 +    def title: String = get_string("title")
    1.33 +    def authors: List[String] = get_strings("author")
    1.34 +    def date: Option[Date] = get("date").map(parse_date(_))
    1.35 +    def topics: List[String] = get_strings("topic")
    1.36 +    def `abstract`: String = get_string("abstract")
    1.37 +    def maintainers: List[String] = get_strings("notify")
    1.38 +    def contributors: List[String] = get_strings("contributors")
    1.39 +    def license: Option[String] = get("license")
    1.40    }
    1.41  }
    1.42