more operations;
authorwenzelm
Wed Oct 05 13:56:19 2016 +0200 (2016-10-05)
changeset 640537ece2e14fd6c
parent 64052 72fa79eab7f6
child 64054 1fc9ab31720d
more operations;
src/Pure/Tools/build_log.scala
     1.1 --- a/src/Pure/Tools/build_log.scala	Wed Oct 05 13:27:25 2016 +0200
     1.2 +++ b/src/Pure/Tools/build_log.scala	Wed Oct 05 13:56:19 2016 +0200
     1.3 @@ -13,6 +13,7 @@
     1.4  
     1.5    object Props
     1.6    {
     1.7 +    def print(props: Properties.T): String = YXML.string_of_body(XML.Encode.properties(props))
     1.8      def parse(text: String): Properties.T = XML.Decode.properties(YXML.parse_body(text))
     1.9  
    1.10      def parse_lines(prefix: String, lines: List[String]): List[Properties.T] =