equal
deleted
inserted
replaced
84 def uncompressed(cache: XZ.Cache = XZ.cache()): Bytes = |
84 def uncompressed(cache: XZ.Cache = XZ.cache()): Bytes = |
85 { |
85 { |
86 val (compressed, bytes) = body.join |
86 val (compressed, bytes) = body.join |
87 if (compressed) bytes.uncompress(cache = cache) else bytes |
87 if (compressed) bytes.uncompress(cache = cache) else bytes |
88 } |
88 } |
|
89 |
|
90 def uncompressed_yxml(cache: XZ.Cache = XZ.cache()): XML.Body = |
|
91 YXML.parse_body(UTF8.decode_permissive(uncompressed(cache = cache))) |
89 } |
92 } |
90 |
93 |
91 def make_regex(pattern: String): Regex = |
94 def make_regex(pattern: String): Regex = |
92 { |
95 { |
93 @tailrec def make(result: List[String], depth: Int, chs: List[Char]): Regex = |
96 @tailrec def make(result: List[String], depth: Int, chs: List[Char]): Regex = |