equal
deleted
inserted
replaced
54 |
54 |
55 object Results |
55 object Results |
56 { |
56 { |
57 type Entry = (Long, XML.Elem) |
57 type Entry = (Long, XML.Elem) |
58 val empty: Results = new Results(SortedMap.empty) |
58 val empty: Results = new Results(SortedMap.empty) |
59 def make(args: TraversableOnce[Results.Entry]): Results = (empty /: args)(_ + _) |
59 def make(args: IterableOnce[Results.Entry]): Results = (empty /: args)(_ + _) |
60 def merge(args: TraversableOnce[Results]): Results = (empty /: args)(_ ++ _) |
60 def merge(args: IterableOnce[Results]): Results = (empty /: args)(_ ++ _) |
61 } |
61 } |
62 |
62 |
63 final class Results private(private val rep: SortedMap[Long, XML.Elem]) |
63 final class Results private(private val rep: SortedMap[Long, XML.Elem]) |
64 { |
64 { |
65 def is_empty: Boolean = rep.isEmpty |
65 def is_empty: Boolean = rep.isEmpty |
90 |
90 |
91 object Exports |
91 object Exports |
92 { |
92 { |
93 type Entry = (Long, Export.Entry) |
93 type Entry = (Long, Export.Entry) |
94 val empty: Exports = new Exports(SortedMap.empty) |
94 val empty: Exports = new Exports(SortedMap.empty) |
95 def merge(args: TraversableOnce[Exports]): Exports = (empty /: args)(_ ++ _) |
95 def merge(args: IterableOnce[Exports]): Exports = (empty /: args)(_ ++ _) |
96 } |
96 } |
97 |
97 |
98 final class Exports private(private val rep: SortedMap[Long, Export.Entry]) |
98 final class Exports private(private val rep: SortedMap[Long, Export.Entry]) |
99 { |
99 { |
100 def is_empty: Boolean = rep.isEmpty |
100 def is_empty: Boolean = rep.isEmpty |
132 object Markups |
132 object Markups |
133 { |
133 { |
134 type Entry = (Markup_Index, Markup_Tree) |
134 type Entry = (Markup_Index, Markup_Tree) |
135 val empty: Markups = new Markups(Map.empty) |
135 val empty: Markups = new Markups(Map.empty) |
136 def init(markup: Markup_Tree): Markups = new Markups(Map(Markup_Index.markup -> markup)) |
136 def init(markup: Markup_Tree): Markups = new Markups(Map(Markup_Index.markup -> markup)) |
137 def make(args: TraversableOnce[Entry]): Markups = (empty /: args)(_ + _) |
137 def make(args: IterableOnce[Entry]): Markups = (empty /: args)(_ + _) |
138 def merge(args: TraversableOnce[Markups]): Markups = (empty /: args)(_ ++ _) |
138 def merge(args: IterableOnce[Markups]): Markups = (empty /: args)(_ ++ _) |
139 } |
139 } |
140 |
140 |
141 final class Markups private(private val rep: Map[Markup_Index, Markup_Tree]) |
141 final class Markups private(private val rep: Map[Markup_Index, Markup_Tree]) |
142 { |
142 { |
143 def is_empty: Boolean = rep.isEmpty |
143 def is_empty: Boolean = rep.isEmpty |