proper treatment of empty extra lines (amending 98a440cfbb2b);
authorwenzelm
Mon Mar 25 15:48:08 2019 +0100 (2 months ago)
changeset 699784ecdd3eaec04
parent 69977 3c166df11085
child 69979 4744e75393d9
proper treatment of empty extra lines (amending 98a440cfbb2b);
src/Pure/Admin/afp.scala
     1.1 --- a/src/Pure/Admin/afp.scala	Mon Mar 25 15:38:56 2019 +0100
     1.2 +++ b/src/Pure/Admin/afp.scala	Mon Mar 25 15:48:08 2019 +0100
     1.3 @@ -77,7 +77,7 @@
     1.4  
     1.5      def flush()
     1.6      {
     1.7 -      if (section != "") result += (section -> props.reverse)
     1.8 +      if (section != "") result += (section -> props.reverse.filter(p => p._2.nonEmpty))
     1.9        section = ""
    1.10        props = Nil
    1.11      }
    1.12 @@ -91,8 +91,7 @@
    1.13          case Section(name) => flush(); section = name
    1.14          case Property(a, b) =>
    1.15            if (section == "") err("Property without a section")
    1.16 -          val c = b.trim
    1.17 -          if (c.nonEmpty) props = (a -> c) :: props
    1.18 +          props = (a -> b.trim) :: props
    1.19          case Extra_Line(line) =>
    1.20            props match {
    1.21              case Nil => err("Extra line without a property")