33 def + (info: XML.Elem): Entry = |
33 def + (info: XML.Elem): Entry = |
34 if (elements(info.markup.name)) copy(rev_markup = info :: rev_markup) |
34 if (elements(info.markup.name)) copy(rev_markup = info :: rev_markup) |
35 else copy(rev_markup = info :: rev_markup, elements = elements + info.markup.name) |
35 else copy(rev_markup = info :: rev_markup, elements = elements + info.markup.name) |
36 |
36 |
37 def markup: List[XML.Elem] = rev_markup.reverse |
37 def markup: List[XML.Elem] = rev_markup.reverse |
|
38 |
|
39 def reverse_markup: Entry = |
|
40 copy(rev_markup = rev_markup.reverse, subtree = subtree.reverse_markup) |
38 } |
41 } |
39 |
42 |
40 object Branches |
43 object Branches |
41 { |
44 { |
42 type T = SortedMap[Text.Range, Entry] |
45 type T = SortedMap[Text.Range, Entry] |
43 val empty: T = SortedMap.empty(Text.Range.Ordering) |
46 val empty: T = SortedMap.empty(Text.Range.Ordering) |
|
47 |
|
48 def reverse_markup(branches: T): T = |
|
49 (empty /: branches.iterator) { case (bs, (r, entry)) => bs + (r -> entry.reverse_markup) } |
44 } |
50 } |
45 } |
51 } |
46 |
52 |
47 |
53 |
48 final class Markup_Tree private(branches: Markup_Tree.Branches.T) |
54 final class Markup_Tree private(branches: Markup_Tree.Branches.T) |
49 { |
55 { |
|
56 import Markup_Tree._ |
|
57 |
50 private def this(branches: Markup_Tree.Branches.T, entry: Markup_Tree.Entry) = |
58 private def this(branches: Markup_Tree.Branches.T, entry: Markup_Tree.Entry) = |
51 this(branches + (entry.range -> entry)) |
59 this(branches + (entry.range -> entry)) |
52 |
60 |
53 |
61 def reverse_markup: Markup_Tree = new Markup_Tree(Branches.reverse_markup(branches)) |
54 import Markup_Tree._ |
|
55 |
62 |
56 override def toString = |
63 override def toString = |
57 branches.toList.map(_._2) match { |
64 branches.toList.map(_._2) match { |
58 case Nil => "Empty" |
65 case Nil => "Empty" |
59 case list => list.mkString("Tree(", ",", ")") |
66 case list => list.mkString("Tree(", ",", ")") |