1 /* Title: Pure/PIDE/markup_node.scala |
|
2 Author: Fabian Immler, TU Munich |
|
3 Author: Makarius |
|
4 |
|
5 Text markup nodes. |
|
6 */ |
|
7 |
|
8 package isabelle |
|
9 |
|
10 |
|
11 import javax.swing.tree.DefaultMutableTreeNode |
|
12 |
|
13 |
|
14 |
|
15 case class Markup_Node(val range: Text.Range, val info: Any) |
|
16 { |
|
17 def fits_into(that: Markup_Node): Boolean = |
|
18 that.range.start <= this.range.start && this.range.stop <= that.range.stop |
|
19 } |
|
20 |
|
21 |
|
22 case class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree]) |
|
23 { |
|
24 private def add(branch: Markup_Tree) = // FIXME avoid sort |
|
25 copy(branches = (branch :: branches).sortWith((a, b) => a.node.range.start < b.node.range.start)) |
|
26 |
|
27 private def remove(bs: List[Markup_Tree]) = |
|
28 copy(branches = branches.filterNot(bs.contains(_))) |
|
29 |
|
30 def + (new_tree: Markup_Tree): Markup_Tree = |
|
31 { |
|
32 val new_node = new_tree.node |
|
33 if (new_node fits_into node) { |
|
34 var inserted = false |
|
35 val new_branches = |
|
36 branches.map(branch => |
|
37 if ((new_node fits_into branch.node) && !inserted) { |
|
38 inserted = true |
|
39 branch + new_tree |
|
40 } |
|
41 else branch) |
|
42 if (!inserted) { |
|
43 // new_tree did not fit into children of this |
|
44 // -> insert between this and its branches |
|
45 val fitting = branches filter(_.node fits_into new_node) |
|
46 (this remove fitting) add ((new_tree /: fitting)(_ + _)) |
|
47 } |
|
48 else copy(branches = new_branches) |
|
49 } |
|
50 else { |
|
51 System.err.println("Ignored nonfitting markup: " + new_node) |
|
52 this |
|
53 } |
|
54 } |
|
55 |
|
56 def flatten: List[Markup_Node] = |
|
57 { |
|
58 var next_x = node.range.start |
|
59 if (branches.isEmpty) List(this.node) |
|
60 else { |
|
61 val filled_gaps = |
|
62 for { |
|
63 child <- branches |
|
64 markups = |
|
65 if (next_x < child.node.range.start) |
|
66 new Markup_Node(Text.Range(next_x, child.node.range.start), node.info) :: child.flatten |
|
67 else child.flatten |
|
68 update = (next_x = child.node.range.stop) |
|
69 markup <- markups |
|
70 } yield markup |
|
71 if (next_x < node.range.stop) |
|
72 filled_gaps ::: List(new Markup_Node(Text.Range(next_x, node.range.stop), node.info)) |
|
73 else filled_gaps |
|
74 } |
|
75 } |
|
76 } |
|
77 |
|
78 |
|
79 case class Markup_Text(val markup: List[Markup_Tree], val content: String) |
|
80 { |
|
81 private val root = new Markup_Tree(new Markup_Node(Text.Range(0, content.length), None), markup) // FIXME !? |
|
82 |
|
83 def + (new_tree: Markup_Tree): Markup_Text = |
|
84 new Markup_Text((root + new_tree).branches, content) |
|
85 |
|
86 def filter(pred: Markup_Node => Boolean): Markup_Text = |
|
87 { |
|
88 def filt(tree: Markup_Tree): List[Markup_Tree] = |
|
89 { |
|
90 val branches = tree.branches.flatMap(filt(_)) |
|
91 if (pred(tree.node)) List(tree.copy(branches = branches)) |
|
92 else branches |
|
93 } |
|
94 new Markup_Text(markup.flatMap(filt(_)), content) |
|
95 } |
|
96 |
|
97 def flatten: List[Markup_Node] = markup.flatten(_.flatten) |
|
98 |
|
99 def swing_tree(swing_node: Markup_Node => DefaultMutableTreeNode): DefaultMutableTreeNode = |
|
100 { |
|
101 def swing(tree: Markup_Tree): DefaultMutableTreeNode = |
|
102 { |
|
103 val node = swing_node(tree.node) |
|
104 tree.branches foreach ((branch: Markup_Tree) => node.add(swing(branch))) |
|
105 node |
|
106 } |
|
107 swing(root) |
|
108 } |
|
109 } |
|