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