src/Pure/Admin/afp.scala
changeset 69977 3c166df11085
parent 69976 98a440cfbb2b
child 69978 4ecdd3eaec04
equal deleted inserted replaced
69976:98a440cfbb2b 69977:3c166df11085
     5 */
     5 */
     6 
     6 
     7 package isabelle
     7 package isabelle
     8 
     8 
     9 
     9 
       
    10 import java.time.{LocalDate, ZoneId}
    10 import scala.collection.immutable.SortedMap
    11 import scala.collection.immutable.SortedMap
    11 
    12 
    12 
    13 
    13 object AFP
    14 object AFP
    14 {
    15 {
    25     new AFP(options, base_dir)
    26     new AFP(options, base_dir)
    26 
    27 
    27 
    28 
    28   /* entries */
    29   /* entries */
    29 
    30 
       
    31   def parse_date(s: String): Date =
       
    32   {
       
    33     val t = Date.Formatter.pattern("uuuu-MM-dd").parse(s)
       
    34     val zone_id = ZoneId.of("Europe/Berlin")
       
    35     Date(LocalDate.from(t).atStartOfDay(zone_id))
       
    36   }
       
    37 
    30   sealed case class Entry(name: String, metadata: Properties.T, sessions: List[String])
    38   sealed case class Entry(name: String, metadata: Properties.T, sessions: List[String])
    31   {
    39   {
    32     def maintainers: List[String] =
    40     def get(prop: String): Option[String] = Properties.get(metadata, prop)
    33       Library.space_explode(',', Properties.get(metadata, "notify").getOrElse("")).
    41     def get_string(prop: String): String = get(prop).getOrElse("")
    34         map(_.trim).filter(_.nonEmpty)
    42     def get_strings(prop: String): List[String] =
       
    43       Library.space_explode(',', get_string(prop)).map(_.trim).filter(_.nonEmpty)
       
    44 
       
    45     def title: String = get_string("title")
       
    46     def authors: List[String] = get_strings("author")
       
    47     def date: Option[Date] = get("date").map(parse_date(_))
       
    48     def topics: List[String] = get_strings("topic")
       
    49     def `abstract`: String = get_string("abstract")
       
    50     def maintainers: List[String] = get_strings("notify")
       
    51     def contributors: List[String] = get_strings("contributors")
       
    52     def license: Option[String] = get("license")
    35   }
    53   }
    36 }
    54 }
    37 
    55 
    38 class AFP private(options: Options, val base_dir: Path)
    56 class AFP private(options: Options, val base_dir: Path)
    39 {
    57 {