equal
deleted
inserted
replaced
77 elements: Elements, |
77 elements: Elements, |
78 subtree: Markup_Tree, |
78 subtree: Markup_Tree, |
79 subtree_elements: Elements) |
79 subtree_elements: Elements) |
80 { |
80 { |
81 def markup: List[XML.Elem] = rev_markup.reverse |
81 def markup: List[XML.Elem] = rev_markup.reverse |
|
82 |
|
83 def filter_markup(pred: String => Boolean): List[XML.Elem] = |
|
84 { |
|
85 var result: List[XML.Elem] = Nil |
|
86 for { elem <- rev_markup; if (pred(elem.name)) } |
|
87 result ::= elem |
|
88 result.toList |
|
89 } |
82 |
90 |
83 def + (markup: Text.Markup): Entry = |
91 def + (markup: Text.Markup): Entry = |
84 copy(rev_markup = markup.info :: rev_markup, elements = elements + markup.info) |
92 copy(rev_markup = markup.info :: rev_markup, elements = elements + markup.info) |
85 |
93 |
86 def \ (markup: Text.Markup): Entry = |
94 def \ (markup: Text.Markup): Entry = |
228 def results(x: A, entry: Entry): Option[A] = |
236 def results(x: A, entry: Entry): Option[A] = |
229 { |
237 { |
230 var y = x |
238 var y = x |
231 var changed = false |
239 var changed = false |
232 for { |
240 for { |
233 elem <- entry.markup |
241 elem <- entry.filter_markup(elements) |
234 if elements(elem.name) |
|
235 y1 <- result(y, Text.Info(entry.range, elem)) |
242 y1 <- result(y, Text.Info(entry.range, elem)) |
236 } { y = y1; changed = true } |
243 } { y = y1; changed = true } |
237 if (changed) Some(y) else None |
244 if (changed) Some(y) else None |
238 } |
245 } |
239 |
246 |