# HG changeset patch
# User wenzelm
# Date 1553519966 -3600
# Node ID a3e3be17dca56c2c304f5277ce4ed8e938b0d542
# Parent  5e82015fa8799904fd173b156f51eddf2183adc4
read AFP metadata for entries;

diff -r 5e82015fa879 -r a3e3be17dca5 src/Pure/Admin/afp.scala
--- a/src/Pure/Admin/afp.scala	Sun Mar 24 20:31:53 2019 +0100
+++ b/src/Pure/Admin/afp.scala	Mon Mar 25 14:19:26 2019 +0100
@@ -21,7 +21,66 @@
   def init(options: Options, base_dir: Path = Path.explode("$AFP_BASE")): AFP =
     new AFP(options, base_dir)
 
-  sealed case class Entry(name: String, sessions: List[String])
+
+  /* metadata */
+
+  object Metadata
+  {
+    private val Section = """^\[(\S+)\]\s*$""".r
+    private val Property = """^(\S+)\s*=(.*)$""".r
+    private val Extra_Line = """^\s+(.*)$""".r
+    private val Blank_Line = """^\s*$""".r
+
+    def read(metadata_file: Path): Map[String, Metadata] =
+    {
+      var result = Map.empty[String, Metadata]
+      var section = ""
+      var props = List.empty[Properties.Entry]
+
+      def flush()
+      {
+        if (section != "") result += (section -> new Metadata(props.reverse))
+        section = ""
+        props = Nil
+      }
+
+      for ((line, i) <- split_lines(File.read(metadata_file)).zipWithIndex)
+      {
+        def err(msg: String): Nothing =
+          error(msg + Position.here(Position.Line_File(i + 1, metadata_file.expand.implode)))
+
+        line match {
+          case Section(name) => flush(); section = name
+          case Property(a, b) =>
+            if (section == "") err("Property without a section")
+            props = (a -> b.trim) :: props
+          case Extra_Line(line) =>
+            props match {
+              case Nil => err("Extra line without a property")
+              case (a, b) :: rest => props = (a, b + "\n" + line.trim) :: rest
+            }
+          case Blank_Line() =>
+          case _ => err("Bad input")
+        }
+      }
+
+      flush()
+      result
+    }
+  }
+
+  class Metadata private[AFP](properties: Properties.T)
+  {
+    override def toString: String =
+      properties.map({ case (a, b) => a + "=" + b }).mkString("Metadata(", ", ", ")")
+
+    def is_empty: Boolean = properties.isEmpty
+  }
+
+
+  /* entries */
+
+  sealed case class Entry(name: String, metadata: Metadata, sessions: List[String])
 }
 
 class AFP private(options: Options, val base_dir: Path)
@@ -31,14 +90,28 @@
   val main_dir: Path = base_dir + Path.explode("thys")
 
 
-  /* entries and sessions */
+  /* entries with metadata and sessions */
 
   val entries: List[AFP.Entry] =
-    (for (name <- Sessions.parse_roots(main_dir + Sessions.ROOTS)) yield {
-      val sessions =
-        Sessions.parse_root_entries(main_dir + Path.explode(name) + Sessions.ROOT).map(_.name)
-      AFP.Entry(name, sessions)
-    }).sortBy(_.name)
+  {
+    val entry_metadata = AFP.Metadata.read(base_dir + Path.explode("metadata/metadata"))
+
+    val entries =
+      (for (name <- Sessions.parse_roots(main_dir + Sessions.ROOTS)) yield {
+        val metadata =
+          entry_metadata.getOrElse(name, error("Entry without metadata: " + quote(name)))
+        val sessions =
+          Sessions.parse_root_entries(main_dir + Path.explode(name) + Sessions.ROOT).map(_.name)
+        AFP.Entry(name, metadata, sessions)
+      }).sortBy(_.name)
+
+    val entry_set = entries.iterator.map(_.name).toSet
+    val extra_metadata =
+      (for ((name, _) <- entry_metadata.iterator if !entry_set(name)) yield name).toList.sorted
+    if (extra_metadata.nonEmpty) error("Meta data without entry: " + commas_quote(extra_metadata))
+
+    entries
+  }
 
   val sessions: List[String] = entries.flatMap(_.sessions)