equal
deleted
inserted
replaced
45 type T = SortedMap[Text.Range, Entry] |
45 type T = SortedMap[Text.Range, Entry] |
46 val empty: T = SortedMap.empty(Text.Range.Ordering) |
46 val empty: T = SortedMap.empty(Text.Range.Ordering) |
47 |
47 |
48 def reverse_markup(branches: T): T = |
48 def reverse_markup(branches: T): T = |
49 (empty /: branches.iterator) { case (bs, (r, entry)) => bs + (r -> entry.reverse_markup) } |
49 (empty /: branches.iterator) { case (bs, (r, entry)) => bs + (r -> entry.reverse_markup) } |
|
50 } |
|
51 |
|
52 |
|
53 /* XML representation */ |
|
54 |
|
55 def from_XML(body: XML.Body): Markup_Tree = |
|
56 { |
|
57 var offset = 0 |
|
58 var markup_tree = empty |
|
59 |
|
60 def traverse(tree: XML.Tree): Unit = |
|
61 tree match { |
|
62 case XML.Elem(markup, trees) => |
|
63 val start = offset |
|
64 trees.foreach(traverse) |
|
65 val stop = offset |
|
66 markup_tree += Text.Info(Text.Range(start, stop), XML.Elem(markup, Nil)) |
|
67 case XML.Text(s) => offset += s.length |
|
68 } |
|
69 body.foreach(traverse) |
|
70 |
|
71 markup_tree.reverse_markup |
50 } |
72 } |
51 } |
73 } |
52 |
74 |
53 |
75 |
54 final class Markup_Tree private(branches: Markup_Tree.Branches.T) |
76 final class Markup_Tree private(branches: Markup_Tree.Branches.T) |