10 import javax.swing.tree.DefaultMutableTreeNode |
10 import javax.swing.tree.DefaultMutableTreeNode |
11 |
11 |
12 import isabelle.proofdocument.ProofDocument |
12 import isabelle.proofdocument.ProofDocument |
13 |
13 |
14 |
14 |
15 class MarkupNode(val start: Int, val stop: Int, val content: String, val info: Any, |
15 class Markup_Node(val start: Int, val stop: Int, val info: Any) |
16 val children: List[MarkupNode]) |
|
17 { |
16 { |
|
17 def fits_into(that: Markup_Node): Boolean = |
|
18 that.start <= this.start && this.stop <= that.stop |
|
19 } |
18 |
20 |
19 def swing_tree(make_node: MarkupNode => DefaultMutableTreeNode): DefaultMutableTreeNode = |
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 = |
20 { |
32 { |
21 val node = make_node(this) |
33 val new_node = new_tree.node |
22 children.foreach(node add _.swing_tree(make_node)) |
34 if (new_node fits_into node) { |
23 node |
|
24 } |
|
25 |
|
26 def set_children(new_children: List[MarkupNode]): MarkupNode = |
|
27 new MarkupNode(start, stop, content, info, new_children) |
|
28 |
|
29 private def add(child: MarkupNode) = // FIXME avoid sort? |
|
30 set_children ((child :: children) sort ((a, b) => a.start < b.start)) |
|
31 |
|
32 def remove(nodes: List[MarkupNode]) = set_children(children -- nodes) |
|
33 |
|
34 def fits_into(node: MarkupNode): Boolean = |
|
35 node.start <= this.start && this.stop <= node.stop |
|
36 |
|
37 def + (new_child: MarkupNode): MarkupNode = |
|
38 { |
|
39 if (new_child fits_into this) { |
|
40 var inserted = false |
35 var inserted = false |
41 val new_children = |
36 val new_branches = |
42 children.map(c => |
37 branches.map(branch => |
43 if ((new_child fits_into c) && !inserted) {inserted = true; c + new_child} |
38 if ((new_node fits_into branch.node) && !inserted) { |
44 else c) |
39 inserted = true |
|
40 branch + new_tree |
|
41 } |
|
42 else branch) |
45 if (!inserted) { |
43 if (!inserted) { |
46 // new_child did not fit into children of this |
44 // new_tree did not fit into children of this |
47 // -> insert new_child between this and its children |
45 // -> insert between this and its branches |
48 val fitting = children filter(_ fits_into new_child) |
46 val fitting = branches filter(_.node fits_into new_node) |
49 (this remove fitting) add ((new_child /: fitting) (_ + _)) |
47 (this remove fitting) add ((new_tree /: fitting)(_ + _)) |
50 } |
48 } |
51 else this set_children new_children |
49 else set_branches(new_branches) |
52 } |
50 } |
53 else { |
51 else { |
54 System.err.println("ignored nonfitting markup: " + new_child) |
52 System.err.println("ignored nonfitting markup: " + new_node) |
55 this |
53 this |
56 } |
54 } |
57 } |
55 } |
58 |
56 |
59 def flatten: List[MarkupNode] = { |
57 def flatten: List[Markup_Node] = |
60 var next_x = start |
58 { |
61 if (children.isEmpty) List(this) |
59 var next_x = node.start |
|
60 if (branches.isEmpty) List(this.node) |
62 else { |
61 else { |
63 val filled_gaps = for { |
62 val filled_gaps = |
64 child <- children |
63 for { |
65 markups = |
64 child <- branches |
66 if (next_x < child.start) { |
65 markups = |
67 // FIXME proper content!? |
66 if (next_x < child.node.start) |
68 new MarkupNode(next_x, child.start, content, info, Nil) :: child.flatten |
67 new Markup_Node(next_x, child.node.start, node.info) :: child.flatten |
69 } |
68 else child.flatten |
70 else child.flatten |
69 update = (next_x = child.node.stop) |
71 update = (next_x = child.stop) |
70 markup <- markups |
72 markup <- markups |
71 } yield markup |
73 } yield markup |
72 if (next_x < node.stop) |
74 if (next_x < stop) |
73 filled_gaps + new Markup_Node(next_x, node.stop, node.info) |
75 filled_gaps + new MarkupNode(next_x, stop, content, info, Nil) // FIXME proper content!? |
|
76 else filled_gaps |
74 else filled_gaps |
77 } |
75 } |
78 } |
76 } |
|
77 } |
79 |
78 |
80 def filter(p: MarkupNode => Boolean): List[MarkupNode] = |
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 = |
81 { |
89 { |
82 val filtered = children.flatMap(_.filter(p)) |
90 def filt(tree: Markup_Tree): List[Markup_Tree] = |
83 if (p(this)) List(this set_children(filtered)) |
91 { |
84 else filtered |
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) |
85 } |
97 } |
86 |
98 |
87 override def toString = |
99 def flatten: List[Markup_Node] = markup.flatten(_.flatten) |
88 "([" + start + " - " + stop + "] ( " + content + "): " + info.toString |
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 } |
89 } |
111 } |