13 import scala.collection.immutable.SortedMap |
13 import scala.collection.immutable.SortedMap |
14 |
14 |
15 |
15 |
16 object Markup_Tree |
16 object Markup_Tree |
17 { |
17 { |
18 sealed case class Cumulate[A](info: A, result: PartialFunction[(A, Text.Markup), A]) |
18 sealed case class Cumulate[A]( |
19 sealed case class Select[A](result: PartialFunction[Text.Markup, A]) |
19 info: A, result: PartialFunction[(A, Text.Markup), A], elements: Option[Set[String]]) |
|
20 sealed case class Select[A]( |
|
21 result: PartialFunction[Text.Markup, A], elements: Option[Set[String]]) |
20 |
22 |
21 val empty: Markup_Tree = new Markup_Tree(Branches.empty) |
23 val empty: Markup_Tree = new Markup_Tree(Branches.empty) |
22 |
24 |
23 object Entry |
25 object Entry |
24 { |
26 { |
25 def apply(markup: Text.Markup, subtree: Markup_Tree): Entry = |
27 def apply(markup: Text.Markup, subtree: Markup_Tree): Entry = |
26 Entry(markup.range, List(markup.info), subtree) |
28 Entry(markup.range, List(markup.info), Set(markup.info.markup.name), subtree) |
27 } |
29 } |
28 |
30 |
29 sealed case class Entry(range: Text.Range, rev_markup: List[XML.Elem], subtree: Markup_Tree) |
31 sealed case class Entry( |
|
32 range: Text.Range, |
|
33 rev_markup: List[XML.Elem], |
|
34 elements: Set[String], |
|
35 subtree: Markup_Tree) |
30 { |
36 { |
31 def + (m: XML.Elem): Entry = copy(rev_markup = m :: rev_markup) |
37 def + (info: XML.Elem): Entry = |
|
38 if (elements(info.markup.name)) copy(rev_markup = info :: rev_markup) |
|
39 else copy(rev_markup = info :: rev_markup, elements = elements + info.markup.name) |
|
40 |
32 def markup: List[XML.Elem] = rev_markup.reverse |
41 def markup: List[XML.Elem] = rev_markup.reverse |
33 } |
42 } |
34 |
43 |
35 object Branches |
44 object Branches |
36 { |
45 { |
100 def cumulate[A](root_range: Text.Range)(body: Cumulate[A]): Stream[Text.Info[A]] = |
109 def cumulate[A](root_range: Text.Range)(body: Cumulate[A]): Stream[Text.Info[A]] = |
101 { |
110 { |
102 val root_info = body.info |
111 val root_info = body.info |
103 |
112 |
104 def result(x: A, entry: Entry): Option[A] = |
113 def result(x: A, entry: Entry): Option[A] = |
105 { |
114 if (body.elements match { case Some(es) => es.exists(entry.elements) case None => true }) { |
106 val (y, changed) = |
115 val (y, changed) = |
107 (entry.markup :\ (x, false))((info, res) => |
116 (entry.markup :\ (x, false))((info, res) => |
108 { |
117 { |
109 val (y, changed) = res |
118 val (y, changed) = res |
110 val arg = (x, Text.Info(entry.range, info)) |
119 val arg = (x, Text.Info(entry.range, info)) |
111 if (body.result.isDefinedAt(arg)) (body.result(arg), true) |
120 if (body.result.isDefinedAt(arg)) (body.result(arg), true) |
112 else res |
121 else res |
113 }) |
122 }) |
114 if (changed) Some(y) else None |
123 if (changed) Some(y) else None |
115 } |
124 } |
|
125 else None |
116 |
126 |
117 def stream( |
127 def stream( |
118 last: Text.Offset, |
128 last: Text.Offset, |
119 stack: List[(Text.Info[A], Stream[(Text.Range, Entry)])]): Stream[Text.Info[A]] = |
129 stack: List[(Text.Info[A], Stream[(Text.Range, Entry)])]): Stream[Text.Info[A]] = |
120 { |
130 { |