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: IterableOnce[Results.Entry]): Results = args.foldLeft(empty)(_ + _) |
59 def make(args: IterableOnce[Results.Entry]): Results = |
60 def merge(args: IterableOnce[Results]): Results = args.foldLeft(empty)(_ ++ _) |
60 args.iterator.foldLeft(empty)(_ + _) |
|
61 def merge(args: IterableOnce[Results]): Results = |
|
62 args.iterator.foldLeft(empty)(_ ++ _) |
61 } |
63 } |
62 |
64 |
63 final class Results private(private val rep: SortedMap[Long, XML.Elem]) |
65 final class Results private(private val rep: SortedMap[Long, XML.Elem]) |
64 { |
66 { |
65 def is_empty: Boolean = rep.isEmpty |
67 def is_empty: Boolean = rep.isEmpty |
90 |
92 |
91 object Exports |
93 object Exports |
92 { |
94 { |
93 type Entry = (Long, Export.Entry) |
95 type Entry = (Long, Export.Entry) |
94 val empty: Exports = new Exports(SortedMap.empty) |
96 val empty: Exports = new Exports(SortedMap.empty) |
95 def merge(args: IterableOnce[Exports]): Exports = args.foldLeft(empty)(_ ++ _) |
97 def merge(args: IterableOnce[Exports]): Exports = |
|
98 args.iterator.foldLeft(empty)(_ ++ _) |
96 } |
99 } |
97 |
100 |
98 final class Exports private(private val rep: SortedMap[Long, Export.Entry]) |
101 final class Exports private(private val rep: SortedMap[Long, Export.Entry]) |
99 { |
102 { |
100 def is_empty: Boolean = rep.isEmpty |
103 def is_empty: Boolean = rep.isEmpty |
132 object Markups |
135 object Markups |
133 { |
136 { |
134 type Entry = (Markup_Index, Markup_Tree) |
137 type Entry = (Markup_Index, Markup_Tree) |
135 val empty: Markups = new Markups(Map.empty) |
138 val empty: Markups = new Markups(Map.empty) |
136 def init(markup: Markup_Tree): Markups = new Markups(Map(Markup_Index.markup -> markup)) |
139 def init(markup: Markup_Tree): Markups = new Markups(Map(Markup_Index.markup -> markup)) |
137 def make(args: IterableOnce[Entry]): Markups = args.foldLeft(empty)(_ + _) |
140 def make(args: IterableOnce[Entry]): Markups = |
138 def merge(args: IterableOnce[Markups]): Markups = args.foldLeft(empty)(_ ++ _) |
141 args.iterator.foldLeft(empty)(_ + _) |
|
142 def merge(args: IterableOnce[Markups]): Markups = |
|
143 args.iterator.foldLeft(empty)(_ ++ _) |
139 } |
144 } |
140 |
145 |
141 final class Markups private(private val rep: Map[Markup_Index, Markup_Tree]) |
146 final class Markups private(private val rep: Map[Markup_Index, Markup_Tree]) |
142 { |
147 { |
143 def is_empty: Boolean = rep.isEmpty |
148 def is_empty: Boolean = rep.isEmpty |