equal
deleted
inserted
replaced
254 /* properties (YXML) */ |
254 /* properties (YXML) */ |
255 |
255 |
256 val xml_cache = new XML.Cache() |
256 val xml_cache = new XML.Cache() |
257 |
257 |
258 def parse_props(text: String): Properties.T = |
258 def parse_props(text: String): Properties.T = |
259 xml_cache.props(Properties.decode_lines(XML.Decode.properties(YXML.parse_body(text)))) |
259 try { |
|
260 xml_cache.props(Properties.decode_lines(XML.Decode.properties(YXML.parse_body(text)))) |
|
261 } |
|
262 catch { case _: XML.Error => log_file.err("malformed properties") } |
260 |
263 |
261 def filter_lines(marker: String): List[String] = |
264 def filter_lines(marker: String): List[String] = |
262 for (line <- lines; s <- Library.try_unprefix(marker, line)) yield s |
265 for (line <- lines; s <- Library.try_unprefix(marker, line)) yield s |
263 |
266 |
264 def filter_props(marker: String): List[Properties.T] = |
267 def filter_props(marker: String): List[Properties.T] = |