clarified multi-line properties;

--- a/src/Pure/Admin/build_history.scala	Fri Apr 28 23:19:06 2017 +0200
+++ b/src/Pure/Admin/build_history.scala	Sat Apr 29 09:38:22 2017 +0200
@@ -211,8 +211,8 @@
       val store = Sessions.store()
 
       val meta_info =
-        Build_Log.Prop.multiple(Build_Log.Prop.build_tags.name, build_tags) :::
-        Build_Log.Prop.multiple(Build_Log.Prop.build_args.name, build_args1) :::
+        Properties.lines_nonempty(Build_Log.Prop.build_tags.name, build_tags) :::
+        Properties.lines_nonempty(Build_Log.Prop.build_args.name, build_args1) :::
         List(
           Build_Log.Prop.build_group_id.name -> build_group_id,
           Build_Log.Prop.build_id.name -> (build_host + ":" + build_start.time.ms),

--- a/src/Pure/Admin/build_log.scala	Fri Apr 28 23:19:06 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Sat Apr 29 09:38:22 2017 +0200
@@ -26,20 +26,8 @@
 
   object Prop
   {
-    val separator = '\u000b'
-
-    def cat_multiple(args: List[String]): String =
-      args.mkString(separator.toString)
-
-    def multiple(name: String, args: List[String]): Properties.T =
-      if (args.isEmpty) Nil
-      else List(name -> cat_multiple(args))
-
-    def multiple_lines(s: String): String =
-      cat_lines(Library.space_explode(separator, s))
-
-    val build_tags = SQL.Column.string("build_tags")  // multiple
-    val build_args = SQL.Column.string("build_args")  // multiple
+    val build_tags = SQL.Column.string("build_tags")  // lines
+    val build_args = SQL.Column.string("build_args")  // lines
     val build_group_id = SQL.Column.string("build_group_id")
     val build_id = SQL.Column.string("build_id")
     val build_engine = SQL.Column.string("build_engine")
@@ -204,7 +192,7 @@
     /* inlined content */
 
     def print_props(marker: String, props: Properties.T): String =
-      marker + YXML.string_of_body(XML.Encode.properties(props))
+      marker + YXML.string_of_body(XML.Encode.properties(Properties.encode_lines(props)))
   }
 
   class Log_File private(val name: String, val lines: List[String])
@@ -260,7 +248,7 @@
     val xml_cache = new XML.Cache()
 
     def parse_props(text: String): Properties.T =
-      xml_cache.props(XML.Decode.properties(YXML.parse_body(text)))
+      xml_cache.props(Properties.decode_lines(XML.Decode.properties(YXML.parse_body(text))))
 
     def filter_props(marker: String): List[Properties.T] =
       for {
@@ -684,7 +672,7 @@
                 if (c.T == SQL.Type.Date)
                   db.set_date(stmt, i + 2, meta_info.get_date(c))
                 else
-                  db.set_string(stmt, i + 2, meta_info.get(c).map(Prop.multiple_lines(_)))
+                  db.set_string(stmt, i + 2, meta_info.get(c))
               }
               stmt.execute()
             })
@@ -706,7 +694,7 @@
               (if (c.T == SQL.Type.Date)
                 db.get(rs, c, db.date _).map(Log_File.Date_Format(_))
                else
-                db.get(rs, c, db.string _).map(s => Prop.cat_multiple(split_lines(s)))))
+                db.get(rs, c, db.string _)))
           val n = Prop.all_props.length
           val props = for ((x, Some(y)) <- results.take(n)) yield (x, y)
           val settings = for ((x, Some(y)) <- results.drop(n)) yield (x, y)

--- a/src/Pure/General/properties.scala	Fri Apr 28 23:19:06 2017 +0200
+++ b/src/Pure/General/properties.scala	Sat Apr 29 09:38:22 2017 +0200
@@ -9,6 +9,8 @@
 
 object Properties
 {
+  /* entries */
+
   type Entry = (java.lang.String, java.lang.String)
   type T = List[Entry]
 
@@ -31,7 +33,21 @@
   }
 
 
-  /* named entries */
+  /* multi-line entries */
+
+  val separator = '\u000b'
+
+  def encode_lines(s: java.lang.String): java.lang.String = s.replace('\n', separator)
+  def decode_lines(s: java.lang.String): java.lang.String = s.replace(separator, '\n')
+
+  def encode_lines(props: T): T = props.map({ case (a, b) => (a, encode_lines(b)) })
+  def decode_lines(props: T): T = props.map({ case (a, b) => (a, decode_lines(b)) })
+
+  def lines_nonempty(x: java.lang.String, ys: List[java.lang.String]): Properties.T =
+    if (ys.isEmpty) Nil else List((x, cat_lines(ys)))
+
+
+  /* entry types */
 
   class String(val name: java.lang.String)
   {