29 { |
29 { |
30 type Entry = (Long, XML.Tree) |
30 type Entry = (Long, XML.Tree) |
31 val empty = new Results(SortedMap.empty) |
31 val empty = new Results(SortedMap.empty) |
32 def make(args: TraversableOnce[Results.Entry]): Results = (empty /: args)(_ + _) |
32 def make(args: TraversableOnce[Results.Entry]): Results = (empty /: args)(_ + _) |
33 def merge(args: TraversableOnce[Results]): Results = (empty /: args)(_ ++ _) |
33 def merge(args: TraversableOnce[Results]): Results = (empty /: args)(_ ++ _) |
|
34 |
|
35 |
|
36 /* XML data representation */ |
|
37 |
|
38 val encode: XML.Encode.T[Results] = (results: Results) => |
|
39 { import XML.Encode._; list(pair(long, tree))(results.rep.toList) } |
|
40 |
|
41 val decode: XML.Decode.T[Results] = (body: XML.Body) => |
|
42 { import XML.Decode._; make(list(pair(long, tree))(body)) } |
34 } |
43 } |
35 |
44 |
36 final class Results private(private val rep: SortedMap[Long, XML.Tree]) |
45 final class Results private(private val rep: SortedMap[Long, XML.Tree]) |
37 { |
46 { |
38 def is_empty: Boolean = rep.isEmpty |
47 def is_empty: Boolean = rep.isEmpty |
69 sealed case class Markup_Index(status: Boolean, chunk_name: Symbol.Text_Chunk.Name) |
78 sealed case class Markup_Index(status: Boolean, chunk_name: Symbol.Text_Chunk.Name) |
70 |
79 |
71 object Markups |
80 object Markups |
72 { |
81 { |
73 val empty: Markups = new Markups(Map.empty) |
82 val empty: Markups = new Markups(Map.empty) |
74 |
83 def init(markup: Markup_Tree): Markups = new Markups(Map(Markup_Index.markup -> markup)) |
75 def init(markup: Markup_Tree): Markups = |
84 def merge(args: TraversableOnce[Markups]): Markups = (empty /: args)(_ ++ _) |
76 new Markups(Map(Markup_Index.markup -> markup)) |
85 |
|
86 |
|
87 /* XML data representation */ |
|
88 |
|
89 def encode(source_length: Int): XML.Encode.T[Markups] = (markups: Markups) => |
|
90 { |
|
91 import XML.Encode._ |
|
92 |
|
93 val markup_index: T[Markup_Index] = (index: Markup_Index) => |
|
94 pair(bool, Symbol.Text_Chunk.encode_name)(index.status, index.chunk_name) |
|
95 |
|
96 val markup_tree: T[Markup_Tree] = |
|
97 _.to_XML(Text.Range(0, source_length), Symbol.spaces(source_length), Markup.Elements.full) |
|
98 |
|
99 list(pair(markup_index, markup_tree))(markups.rep.toList) |
|
100 } |
|
101 |
|
102 val decode: XML.Decode.T[Markups] = (body: XML.Body) => |
|
103 { |
|
104 import XML.Decode._ |
|
105 |
|
106 val markup_index: T[Markup_Index] = (body: XML.Body) => |
|
107 { |
|
108 val (status, chunk_name) = pair(bool, Symbol.Text_Chunk.decode_name)(body) |
|
109 Markup_Index(status, chunk_name) |
|
110 } |
|
111 |
|
112 (Markups.empty /: list(pair(markup_index, Markup_Tree.from_XML(_)))(body))(_ + _) |
|
113 } |
77 } |
114 } |
78 |
115 |
79 final class Markups private(private val rep: Map[Markup_Index, Markup_Tree]) |
116 final class Markups private(private val rep: Map[Markup_Index, Markup_Tree]) |
80 { |
117 { |
81 def is_empty: Boolean = rep.isEmpty |
118 def is_empty: Boolean = rep.isEmpty |
83 def apply(index: Markup_Index): Markup_Tree = |
120 def apply(index: Markup_Index): Markup_Tree = |
84 rep.getOrElse(index, Markup_Tree.empty) |
121 rep.getOrElse(index, Markup_Tree.empty) |
85 |
122 |
86 def add(index: Markup_Index, markup: Text.Markup): Markups = |
123 def add(index: Markup_Index, markup: Text.Markup): Markups = |
87 new Markups(rep + (index -> (this(index) + markup))) |
124 new Markups(rep + (index -> (this(index) + markup))) |
|
125 |
|
126 def + (entry: (Markup_Index, Markup_Tree)): Markups = |
|
127 { |
|
128 val (index, tree) = entry |
|
129 new Markups(rep + (index -> (this(index).merge(tree, Text.Range.full, Markup.Elements.full)))) |
|
130 } |
|
131 |
|
132 def ++ (other: Markups): Markups = |
|
133 if (this eq other) this |
|
134 else if (rep.isEmpty) other |
|
135 else (this /: other.rep.iterator)(_ + _) |
88 |
136 |
89 def redirection_iterator: Iterator[Document_ID.Generic] = |
137 def redirection_iterator: Iterator[Document_ID.Generic] = |
90 for (Markup_Index(_, Symbol.Text_Chunk.Id(id)) <- rep.keysIterator) |
138 for (Markup_Index(_, Symbol.Text_Chunk.Id(id)) <- rep.keysIterator) |
91 yield id |
139 yield id |
92 |
140 |
112 |
160 |
113 /* state */ |
161 /* state */ |
114 |
162 |
115 object State |
163 object State |
116 { |
164 { |
117 def merge_results(states: List[State]): Command.Results = |
165 def merge_results(states: List[State]): Results = |
118 Results.merge(states.map(_.results)) |
166 Results.merge(states.map(_.results)) |
|
167 |
|
168 def merge_markups(states: List[State]): Markups = |
|
169 Markups.merge(states.map(_.markups)) |
119 |
170 |
120 def merge_markup(states: List[State], index: Markup_Index, |
171 def merge_markup(states: List[State], index: Markup_Index, |
121 range: Text.Range, elements: Markup.Elements): Markup_Tree = |
172 range: Text.Range, elements: Markup.Elements): Markup_Tree = |
122 Markup_Tree.merge(states.map(_.markup(index)), range, elements) |
173 Markup_Tree.merge(states.map(_.markup(index)), range, elements) |
|
174 |
|
175 def merge(command: Command, states: List[State]): State = |
|
176 State(command, states.flatMap(_.status), merge_results(states), merge_markups(states)) |
|
177 |
|
178 |
|
179 /* XML data representation */ |
|
180 |
|
181 val encode: XML.Encode.T[State] = (st: State) => |
|
182 { |
|
183 import XML.Encode._ |
|
184 |
|
185 val command = st.command |
|
186 val blobs_names = command.blobs_names.map(_.node) |
|
187 val blobs_index = command.blobs_index |
|
188 require(command.blobs_ok) |
|
189 |
|
190 pair(long, pair(string, pair(pair(list(string), int), pair(Command_Span.encode, |
|
191 pair(list(Markup.encode), pair(Results.encode, Markups.encode(command.source.length)))))))( |
|
192 (command.id, (command.node_name.node, ((blobs_names, blobs_index), (command.span, |
|
193 (st.status, (st.results, st.markups))))))) |
|
194 } |
|
195 |
|
196 def decode(node_name: String => Document.Node.Name): XML.Decode.T[State] = (body: XML.Body) => |
|
197 { |
|
198 import XML.Decode._ |
|
199 val (id, (node, ((blobs_names, blobs_index), (span, (status, (results, markups)))))) = |
|
200 pair(long, pair(string, pair(pair(list(string), int), pair(Command_Span.decode, |
|
201 pair(list(Markup.decode), pair(Results.decode, Markups.decode))))))(body) |
|
202 |
|
203 val blobs_info: Blobs_Info = |
|
204 (blobs_names.map(name => Exn.Res((node_name(name), None)): Blob), blobs_index) |
|
205 val command = Command(id, node_name(node), blobs_info, span) |
|
206 State(command, status, results, markups) |
|
207 } |
123 } |
208 } |
124 |
209 |
125 sealed case class State( |
210 sealed case class State( |
126 command: Command, |
211 command: Command, |
127 status: List[Markup] = Nil, |
212 status: List[Markup] = Nil, |
402 /* blobs */ |
487 /* blobs */ |
403 |
488 |
404 def blobs: List[Command.Blob] = blobs_info._1 |
489 def blobs: List[Command.Blob] = blobs_info._1 |
405 def blobs_index: Int = blobs_info._2 |
490 def blobs_index: Int = blobs_info._2 |
406 |
491 |
|
492 def blobs_ok: Boolean = |
|
493 blobs.forall({ case Exn.Res(_) => true case _ => false }) |
|
494 |
407 def blobs_names: List[Document.Node.Name] = |
495 def blobs_names: List[Document.Node.Name] = |
408 for (Exn.Res((name, _)) <- blobs) yield name |
496 for (Exn.Res((name, _)) <- blobs) yield name |
409 |
497 |
410 def blobs_undefined: List[Document.Node.Name] = |
498 def blobs_undefined: List[Document.Node.Name] = |
411 for (Exn.Res((name, None)) <- blobs) yield name |
499 for (Exn.Res((name, None)) <- blobs) yield name |