proper treatment of empty extra lines (amending 98a440cfbb2b);

--- a/src/Pure/Admin/afp.scala	Mon Mar 25 15:38:56 2019 +0100
+++ b/src/Pure/Admin/afp.scala	Mon Mar 25 15:48:08 2019 +0100
@@ -77,7 +77,7 @@
 
     def flush()
     {
-      if (section != "") result += (section -> props.reverse)
+      if (section != "") result += (section -> props.reverse.filter(p => p._2.nonEmpty))
       section = ""
       props = Nil
     }
@@ -91,8 +91,7 @@
         case Section(name) => flush(); section = name
         case Property(a, b) =>
           if (section == "") err("Property without a section")
-          val c = b.trim
-          if (c.nonEmpty) props = (a -> c) :: props
+          props = (a -> b.trim) :: props
         case Extra_Line(line) =>
           props match {
             case Nil => err("Extra line without a property")