64 } |
64 } |
65 |
65 |
66 |
66 |
67 /* XML representation */ |
67 /* XML representation */ |
68 |
68 |
69 // FIXME decode markup body |
69 @tailrec private def strip_elems( |
70 @tailrec private def strip_elems(markups: List[Markup], body: XML.Body): (List[Markup], XML.Body) = |
70 elems: List[XML.Elem], body: XML.Body): (List[XML.Elem], XML.Body) = |
71 body match { |
71 body match { |
72 case List(XML.Elem(markup1, body1)) => strip_elems(markup1 :: markups, body1) |
72 case List(XML.Wrapped_Elem(markup1, body1, body2)) => |
73 case _ => (markups, body) |
73 strip_elems(XML.Elem(markup1, body1) :: elems, body2) |
|
74 case List(XML.Elem(markup1, body1)) => |
|
75 strip_elems(XML.Elem(markup1, Nil) :: elems, body1) |
|
76 case _ => (elems, body) |
74 } |
77 } |
75 |
78 |
76 private def make_trees(acc: (Int, List[Markup_Tree]), tree: XML.Tree): (Int, List[Markup_Tree]) = |
79 private def make_trees(acc: (Int, List[Markup_Tree]), tree: XML.Tree): (Int, List[Markup_Tree]) = |
77 { |
80 { |
78 val (offset, markup_trees) = acc |
81 val (offset, markup_trees) = acc |
82 (offset + XML.text_length(body), markup_trees) |
85 (offset + XML.text_length(body), markup_trees) |
83 |
86 |
84 case (elems, body) => |
87 case (elems, body) => |
85 val (end_offset, subtrees) = ((offset, Nil: List[Markup_Tree]) /: body)(make_trees) |
88 val (end_offset, subtrees) = ((offset, Nil: List[Markup_Tree]) /: body)(make_trees) |
86 val range = Text.Range(offset, end_offset) |
89 val range = Text.Range(offset, end_offset) |
87 val entry = Entry(range, elems.map(XML.Elem(_, Nil)), merge_disjoint(subtrees)) |
90 val entry = Entry(range, elems, merge_disjoint(subtrees)) |
88 (end_offset, new Markup_Tree(Branches.empty, entry) :: markup_trees) |
91 (end_offset, new Markup_Tree(Branches.empty, entry) :: markup_trees) |
89 } |
92 } |
90 } |
93 } |
91 |
94 |
92 def from_XML(body: XML.Body): Markup_Tree = |
95 def from_XML(body: XML.Body): Markup_Tree = |
150 if (start == stop) Nil |
153 if (start == stop) Nil |
151 else List(XML.Text(text.subSequence(start, stop).toString)) |
154 else List(XML.Text(text.subSequence(start, stop).toString)) |
152 |
155 |
153 def make_elems(rev_markups: List[XML.Elem], body: XML.Body): XML.Body = |
156 def make_elems(rev_markups: List[XML.Elem], body: XML.Body): XML.Body = |
154 (body /: rev_markups) { |
157 (body /: rev_markups) { |
155 case (b, elem) => // FIXME encode markup body |
158 case (b, elem) => |
156 if (filter(elem)) List(XML.Elem(elem.markup, b)) else b |
159 if (!filter(elem)) b |
|
160 else if (elem.body.isEmpty) List(XML.Elem(elem.markup, b)) |
|
161 else List(XML.Wrapped_Elem(elem.markup, elem.body, b)) |
157 } |
162 } |
158 |
163 |
159 def make_body(elem_range: Text.Range, elem_markup: List[XML.Elem], entries: Branches.T) |
164 def make_body(elem_range: Text.Range, elem_markup: List[XML.Elem], entries: Branches.T) |
160 : XML.Body = |
165 : XML.Body = |
161 { |
166 { |