equal
deleted
inserted
replaced
11 { |
11 { |
12 /* inlined properties (YXML) */ |
12 /* inlined properties (YXML) */ |
13 |
13 |
14 object Props |
14 object Props |
15 { |
15 { |
|
16 def print(props: Properties.T): String = YXML.string_of_body(XML.Encode.properties(props)) |
16 def parse(text: String): Properties.T = XML.Decode.properties(YXML.parse_body(text)) |
17 def parse(text: String): Properties.T = XML.Decode.properties(YXML.parse_body(text)) |
17 |
18 |
18 def parse_lines(prefix: String, lines: List[String]): List[Properties.T] = |
19 def parse_lines(prefix: String, lines: List[String]): List[Properties.T] = |
19 for (line <- lines; s <- Library.try_unprefix(prefix, line)) yield parse(s) |
20 for (line <- lines; s <- Library.try_unprefix(prefix, line)) yield parse(s) |
20 |
21 |