tuned;
authorwenzelm
Mon Mar 25 14:40:28 2019 +0100 (3 months ago)
changeset 6997535cc58a54ffc
parent 69974 916726680a66
child 69976 98a440cfbb2b
tuned;
src/Pure/Admin/afp.scala
     1.1 --- a/src/Pure/Admin/afp.scala	Mon Mar 25 14:32:33 2019 +0100
     1.2 +++ b/src/Pure/Admin/afp.scala	Mon Mar 25 14:40:28 2019 +0100
     1.3 @@ -25,65 +25,9 @@
     1.4      new AFP(options, base_dir)
     1.5  
     1.6  
     1.7 -  /* metadata */
     1.8 -
     1.9 -  object Metadata
    1.10 -  {
    1.11 -    private val Section = """^\[(\S+)\]\s*$""".r
    1.12 -    private val Property = """^(\S+)\s*=(.*)$""".r
    1.13 -    private val Extra_Line = """^\s+(.*)$""".r
    1.14 -    private val Blank_Line = """^\s*$""".r
    1.15 -
    1.16 -    def read(metadata_file: Path): Map[String, Metadata] =
    1.17 -    {
    1.18 -      var result = Map.empty[String, Metadata]
    1.19 -      var section = ""
    1.20 -      var props = List.empty[Properties.Entry]
    1.21 -
    1.22 -      def flush()
    1.23 -      {
    1.24 -        if (section != "") result += (section -> new Metadata(props.reverse))
    1.25 -        section = ""
    1.26 -        props = Nil
    1.27 -      }
    1.28 -
    1.29 -      for ((line, i) <- split_lines(File.read(metadata_file)).zipWithIndex)
    1.30 -      {
    1.31 -        def err(msg: String): Nothing =
    1.32 -          error(msg + Position.here(Position.Line_File(i + 1, metadata_file.expand.implode)))
    1.33 -
    1.34 -        line match {
    1.35 -          case Section(name) => flush(); section = name
    1.36 -          case Property(a, b) =>
    1.37 -            if (section == "") err("Property without a section")
    1.38 -            props = (a -> b.trim) :: props
    1.39 -          case Extra_Line(line) =>
    1.40 -            props match {
    1.41 -              case Nil => err("Extra line without a property")
    1.42 -              case (a, b) :: rest => props = (a, b + "\n" + line.trim) :: rest
    1.43 -            }
    1.44 -          case Blank_Line() =>
    1.45 -          case _ => err("Bad input")
    1.46 -        }
    1.47 -      }
    1.48 -
    1.49 -      flush()
    1.50 -      result
    1.51 -    }
    1.52 -  }
    1.53 -
    1.54 -  class Metadata private[AFP](properties: Properties.T)
    1.55 -  {
    1.56 -    override def toString: String =
    1.57 -      properties.map({ case (a, b) => a + "=" + b }).mkString("Metadata(", ", ", ")")
    1.58 -
    1.59 -    def is_empty: Boolean = properties.isEmpty
    1.60 -  }
    1.61 -
    1.62 -
    1.63    /* entries */
    1.64  
    1.65 -  sealed case class Entry(name: String, metadata: Metadata, sessions: List[String])
    1.66 +  sealed case class Entry(name: String, metadata: Properties.T, sessions: List[String])
    1.67  }
    1.68  
    1.69  class AFP private(options: Options, val base_dir: Path)
    1.70 @@ -93,12 +37,57 @@
    1.71    val main_dir: Path = base_dir + Path.explode("thys")
    1.72  
    1.73  
    1.74 +  /* metadata */
    1.75 +
    1.76 +  private val entry_metadata: Map[String, Properties.T] =
    1.77 +  {
    1.78 +    val metadata_file = base_dir + Path.explode("metadata/metadata")
    1.79 +
    1.80 +    var result = Map.empty[String, Properties.T]
    1.81 +    var section = ""
    1.82 +    var props = List.empty[Properties.Entry]
    1.83 +
    1.84 +    val Section = """^\[(\S+)\]\s*$""".r
    1.85 +    val Property = """^(\S+)\s*=(.*)$""".r
    1.86 +    val Extra_Line = """^\s+(.*)$""".r
    1.87 +    val Blank_Line = """^\s*$""".r
    1.88 +
    1.89 +    def flush()
    1.90 +    {
    1.91 +      if (section != "") result += (section -> props.reverse)
    1.92 +      section = ""
    1.93 +      props = Nil
    1.94 +    }
    1.95 +
    1.96 +    for ((line, i) <- split_lines(File.read(metadata_file)).zipWithIndex)
    1.97 +    {
    1.98 +      def err(msg: String): Nothing =
    1.99 +        error(msg + Position.here(Position.Line_File(i + 1, metadata_file.expand.implode)))
   1.100 +
   1.101 +      line match {
   1.102 +        case Section(name) => flush(); section = name
   1.103 +        case Property(a, b) =>
   1.104 +          if (section == "") err("Property without a section")
   1.105 +          props = (a -> b.trim) :: props
   1.106 +        case Extra_Line(line) =>
   1.107 +          props match {
   1.108 +            case Nil => err("Extra line without a property")
   1.109 +            case (a, b) :: rest => props = (a, b + "\n" + line.trim) :: rest
   1.110 +          }
   1.111 +        case Blank_Line() =>
   1.112 +        case _ => err("Bad input")
   1.113 +      }
   1.114 +    }
   1.115 +
   1.116 +    flush()
   1.117 +    result
   1.118 +  }
   1.119 +
   1.120 +
   1.121    /* entries and sessions */
   1.122  
   1.123    val entries_map: SortedMap[String, AFP.Entry] =
   1.124    {
   1.125 -    val entry_metadata = AFP.Metadata.read(base_dir + Path.explode("metadata/metadata"))
   1.126 -
   1.127      val entries =
   1.128        for (name <- Sessions.parse_roots(main_dir + Sessions.ROOTS)) yield {
   1.129          val metadata =