10 |
10 |
11 import javax.swing.tree.DefaultMutableTreeNode |
11 import javax.swing.tree.DefaultMutableTreeNode |
12 |
12 |
13 |
13 |
14 |
14 |
15 case class Markup_Node(val start: Int, val stop: Int, val info: Any) |
15 case class Markup_Node(val range: Text.Range, val info: Any) |
16 { |
16 { |
17 def fits_into(that: Markup_Node): Boolean = |
17 def fits_into(that: Markup_Node): Boolean = |
18 that.start <= this.start && this.stop <= that.stop |
18 that.range.start <= this.range.start && this.range.stop <= that.range.stop |
19 } |
19 } |
20 |
20 |
21 |
21 |
22 case class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree]) |
22 case class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree]) |
23 { |
23 { |
24 private def add(branch: Markup_Tree) = // FIXME avoid sort |
24 private def add(branch: Markup_Tree) = // FIXME avoid sort |
25 copy(branches = (branch :: branches).sortWith((a, b) => a.node.start < b.node.start)) |
25 copy(branches = (branch :: branches).sortWith((a, b) => a.node.range.start < b.node.range.start)) |
26 |
26 |
27 private def remove(bs: List[Markup_Tree]) = |
27 private def remove(bs: List[Markup_Tree]) = |
28 copy(branches = branches.filterNot(bs.contains(_))) |
28 copy(branches = branches.filterNot(bs.contains(_))) |
29 |
29 |
30 def + (new_tree: Markup_Tree): Markup_Tree = |
30 def + (new_tree: Markup_Tree): Markup_Tree = |
53 } |
53 } |
54 } |
54 } |
55 |
55 |
56 def flatten: List[Markup_Node] = |
56 def flatten: List[Markup_Node] = |
57 { |
57 { |
58 var next_x = node.start |
58 var next_x = node.range.start |
59 if (branches.isEmpty) List(this.node) |
59 if (branches.isEmpty) List(this.node) |
60 else { |
60 else { |
61 val filled_gaps = |
61 val filled_gaps = |
62 for { |
62 for { |
63 child <- branches |
63 child <- branches |
64 markups = |
64 markups = |
65 if (next_x < child.node.start) |
65 if (next_x < child.node.range.start) |
66 new Markup_Node(next_x, child.node.start, node.info) :: child.flatten |
66 new Markup_Node(Text.Range(next_x, child.node.range.start), node.info) :: child.flatten |
67 else child.flatten |
67 else child.flatten |
68 update = (next_x = child.node.stop) |
68 update = (next_x = child.node.range.stop) |
69 markup <- markups |
69 markup <- markups |
70 } yield markup |
70 } yield markup |
71 if (next_x < node.stop) |
71 if (next_x < node.range.stop) |
72 filled_gaps ::: List(new Markup_Node(next_x, node.stop, node.info)) |
72 filled_gaps ::: List(new Markup_Node(Text.Range(next_x, node.range.stop), node.info)) |
73 else filled_gaps |
73 else filled_gaps |
74 } |
74 } |
75 } |
75 } |
76 } |
76 } |
77 |
77 |
78 |
78 |
79 case class Markup_Text(val markup: List[Markup_Tree], val content: String) |
79 case class Markup_Text(val markup: List[Markup_Tree], val content: String) |
80 { |
80 { |
81 private val root = new Markup_Tree(new Markup_Node(0, content.length, None), markup) // FIXME !? |
81 private val root = new Markup_Tree(new Markup_Node(Text.Range(0, content.length), None), markup) // FIXME !? |
82 |
82 |
83 def + (new_tree: Markup_Tree): Markup_Text = |
83 def + (new_tree: Markup_Tree): Markup_Text = |
84 new Markup_Text((root + new_tree).branches, content) |
84 new Markup_Text((root + new_tree).branches, content) |
85 |
85 |
86 def filter(pred: Markup_Node => Boolean): Markup_Text = |
86 def filter(pred: Markup_Node => Boolean): Markup_Text = |