src/Pure/Admin/afp.scala
changeset 69973 a3e3be17dca5
parent 69787 60b5a4731695
child 69974 916726680a66
     1.1 --- a/src/Pure/Admin/afp.scala	Sun Mar 24 20:31:53 2019 +0100
     1.2 +++ b/src/Pure/Admin/afp.scala	Mon Mar 25 14:19:26 2019 +0100
     1.3 @@ -21,7 +21,66 @@
     1.4    def init(options: Options, base_dir: Path = Path.explode("$AFP_BASE")): AFP =
     1.5      new AFP(options, base_dir)
     1.6  
     1.7 -  sealed case class Entry(name: String, sessions: List[String])
     1.8 +
     1.9 +  /* metadata */
    1.10 +
    1.11 +  object Metadata
    1.12 +  {
    1.13 +    private val Section = """^\[(\S+)\]\s*$""".r
    1.14 +    private val Property = """^(\S+)\s*=(.*)$""".r
    1.15 +    private val Extra_Line = """^\s+(.*)$""".r
    1.16 +    private val Blank_Line = """^\s*$""".r
    1.17 +
    1.18 +    def read(metadata_file: Path): Map[String, Metadata] =
    1.19 +    {
    1.20 +      var result = Map.empty[String, Metadata]
    1.21 +      var section = ""
    1.22 +      var props = List.empty[Properties.Entry]
    1.23 +
    1.24 +      def flush()
    1.25 +      {
    1.26 +        if (section != "") result += (section -> new Metadata(props.reverse))
    1.27 +        section = ""
    1.28 +        props = Nil
    1.29 +      }
    1.30 +
    1.31 +      for ((line, i) <- split_lines(File.read(metadata_file)).zipWithIndex)
    1.32 +      {
    1.33 +        def err(msg: String): Nothing =
    1.34 +          error(msg + Position.here(Position.Line_File(i + 1, metadata_file.expand.implode)))
    1.35 +
    1.36 +        line match {
    1.37 +          case Section(name) => flush(); section = name
    1.38 +          case Property(a, b) =>
    1.39 +            if (section == "") err("Property without a section")
    1.40 +            props = (a -> b.trim) :: props
    1.41 +          case Extra_Line(line) =>
    1.42 +            props match {
    1.43 +              case Nil => err("Extra line without a property")
    1.44 +              case (a, b) :: rest => props = (a, b + "\n" + line.trim) :: rest
    1.45 +            }
    1.46 +          case Blank_Line() =>
    1.47 +          case _ => err("Bad input")
    1.48 +        }
    1.49 +      }
    1.50 +
    1.51 +      flush()
    1.52 +      result
    1.53 +    }
    1.54 +  }
    1.55 +
    1.56 +  class Metadata private[AFP](properties: Properties.T)
    1.57 +  {
    1.58 +    override def toString: String =
    1.59 +      properties.map({ case (a, b) => a + "=" + b }).mkString("Metadata(", ", ", ")")
    1.60 +
    1.61 +    def is_empty: Boolean = properties.isEmpty
    1.62 +  }
    1.63 +
    1.64 +
    1.65 +  /* entries */
    1.66 +
    1.67 +  sealed case class Entry(name: String, metadata: Metadata, sessions: List[String])
    1.68  }
    1.69  
    1.70  class AFP private(options: Options, val base_dir: Path)
    1.71 @@ -31,14 +90,28 @@
    1.72    val main_dir: Path = base_dir + Path.explode("thys")
    1.73  
    1.74  
    1.75 -  /* entries and sessions */
    1.76 +  /* entries with metadata and sessions */
    1.77  
    1.78    val entries: List[AFP.Entry] =
    1.79 -    (for (name <- Sessions.parse_roots(main_dir + Sessions.ROOTS)) yield {
    1.80 -      val sessions =
    1.81 -        Sessions.parse_root_entries(main_dir + Path.explode(name) + Sessions.ROOT).map(_.name)
    1.82 -      AFP.Entry(name, sessions)
    1.83 -    }).sortBy(_.name)
    1.84 +  {
    1.85 +    val entry_metadata = AFP.Metadata.read(base_dir + Path.explode("metadata/metadata"))
    1.86 +
    1.87 +    val entries =
    1.88 +      (for (name <- Sessions.parse_roots(main_dir + Sessions.ROOTS)) yield {
    1.89 +        val metadata =
    1.90 +          entry_metadata.getOrElse(name, error("Entry without metadata: " + quote(name)))
    1.91 +        val sessions =
    1.92 +          Sessions.parse_root_entries(main_dir + Path.explode(name) + Sessions.ROOT).map(_.name)
    1.93 +        AFP.Entry(name, metadata, sessions)
    1.94 +      }).sortBy(_.name)
    1.95 +
    1.96 +    val entry_set = entries.iterator.map(_.name).toSet
    1.97 +    val extra_metadata =
    1.98 +      (for ((name, _) <- entry_metadata.iterator if !entry_set(name)) yield name).toList.sorted
    1.99 +    if (extra_metadata.nonEmpty) error("Meta data without entry: " + commas_quote(extra_metadata))
   1.100 +
   1.101 +    entries
   1.102 +  }
   1.103  
   1.104    val sessions: List[String] = entries.flatMap(_.sessions)
   1.105