equal
deleted
inserted
replaced
96 new Path(norm_elems(explode_elems(raw_elems) ++ roots)) |
96 new Path(norm_elems(explode_elems(raw_elems) ++ roots)) |
97 } |
97 } |
98 |
98 |
99 def split(str: String): List[Path] = |
99 def split(str: String): List[Path] = |
100 space_explode(':', str).filterNot(_.isEmpty).map(explode) |
100 space_explode(':', str).filterNot(_.isEmpty).map(explode) |
|
101 |
|
102 |
|
103 /* encode */ |
|
104 |
|
105 val encode: XML.Encode.T[Path] = (path => XML.Encode.string(path.implode)) |
101 } |
106 } |
102 |
107 |
103 |
108 |
104 final class Path private(private val elems: List[Path.Elem]) // reversed elements |
109 final class Path private(private val elems: List[Path.Elem]) // reversed elements |
105 { |
110 { |