author | wenzelm |
Wed, 05 May 2010 22:23:45 +0200 | |
changeset 36676 | ac7961d42ac3 |
parent 36012 | src/Pure/Thy/markup_node.scala@0614676f14d4 |
child 36680 | 82f81d128111 |
permissions | -rw-r--r-- |
36676 | 1 |
/* Title: Pure/PIDE/markup_node.scala |
2 |
Author: Fabian Immler, TU Munich |
|
3 |
Author: Makarius |
|
4 |
||
5 |
Document markup nodes, with connection to Swing tree model. |
|
6 |
*/ |
|
34393 | 7 |
|
34871
e596a0b71f3c
incorporate "proofdocument" part into main Isabelle/Pure.jar -- except for html_panel.scala, which depends on external library (Lobo/Cobra browser);
wenzelm
parents:
34760
diff
changeset
|
8 |
package isabelle |
34393 | 9 |
|
34701
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34676
diff
changeset
|
10 |
|
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34676
diff
changeset
|
11 |
import javax.swing.tree.DefaultMutableTreeNode |
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34676
diff
changeset
|
12 |
|
34554
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34517
diff
changeset
|
13 |
|
34393 | 14 |
|
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
15 |
class Markup_Node(val start: Int, val stop: Int, val info: Any) |
34582 | 16 |
{ |
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
17 |
def fits_into(that: Markup_Node): Boolean = |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
18 |
that.start <= this.start && this.stop <= that.stop |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
19 |
} |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
20 |
|
34656 | 21 |
|
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
22 |
class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree]) |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
23 |
{ |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
24 |
def set_branches(bs: List[Markup_Tree]): Markup_Tree = new Markup_Tree(node, bs) |
34557 | 25 |
|
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
26 |
private def add(branch: Markup_Tree) = // FIXME avoid sort |
36012 | 27 |
set_branches((branch :: branches).sortWith((a, b) => a.node.start < b.node.start)) |
34514
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
28 |
|
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
29 |
private def remove(bs: List[Markup_Tree]) = set_branches(branches -- bs) |
34393 | 30 |
|
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
31 |
def + (new_tree: Markup_Tree): Markup_Tree = |
34703 | 32 |
{ |
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
33 |
val new_node = new_tree.node |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
34 |
if (new_node fits_into node) { |
34703 | 35 |
var inserted = false |
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
36 |
val new_branches = |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
37 |
branches.map(branch => |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
38 |
if ((new_node fits_into branch.node) && !inserted) { |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
39 |
inserted = true |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
40 |
branch + new_tree |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
41 |
} |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
42 |
else branch) |
34703 | 43 |
if (!inserted) { |
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
44 |
// new_tree did not fit into children of this |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
45 |
// -> insert between this and its branches |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
46 |
val fitting = branches filter(_.node fits_into new_node) |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
47 |
(this remove fitting) add ((new_tree /: fitting)(_ + _)) |
34703 | 48 |
} |
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
49 |
else set_branches(new_branches) |
34703 | 50 |
} |
51 |
else { |
|
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
52 |
System.err.println("ignored nonfitting markup: " + new_node) |
34703 | 53 |
this |
54 |
} |
|
55 |
} |
|
56 |
||
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
57 |
def flatten: List[Markup_Node] = |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
58 |
{ |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
59 |
var next_x = node.start |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
60 |
if (branches.isEmpty) List(this.node) |
34514
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
61 |
else { |
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
62 |
val filled_gaps = |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
63 |
for { |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
64 |
child <- branches |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
65 |
markups = |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
66 |
if (next_x < child.node.start) |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
67 |
new Markup_Node(next_x, child.node.start, node.info) :: child.flatten |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
68 |
else child.flatten |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
69 |
update = (next_x = child.node.stop) |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
70 |
markup <- markups |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
71 |
} yield markup |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
72 |
if (next_x < node.stop) |
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34871
diff
changeset
|
73 |
filled_gaps ::: List(new Markup_Node(next_x, node.stop, node.info)) |
34514
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
74 |
else filled_gaps |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
75 |
} |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
76 |
} |
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
77 |
} |
34514
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
78 |
|
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
79 |
|
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
80 |
class Markup_Text(val markup: List[Markup_Tree], val content: String) |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
81 |
{ |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
82 |
private lazy val root = |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
83 |
new Markup_Tree(new Markup_Node(0, content.length, None), markup) |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
84 |
|
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
85 |
def + (new_tree: Markup_Tree): Markup_Text = |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
86 |
new Markup_Text((root + new_tree).branches, content) |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
87 |
|
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
88 |
def filter(pred: Markup_Node => Boolean): Markup_Text = |
34701
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34676
diff
changeset
|
89 |
{ |
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
90 |
def filt(tree: Markup_Tree): List[Markup_Tree] = |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
91 |
{ |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
92 |
val branches = tree.branches.flatMap(filt(_)) |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
93 |
if (pred(tree.node)) List(tree.set_branches(branches)) |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
94 |
else branches |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
95 |
} |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
96 |
new Markup_Text(markup.flatMap(filt(_)), content) |
34559 | 97 |
} |
98 |
||
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
99 |
def flatten: List[Markup_Node] = markup.flatten(_.flatten) |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
100 |
|
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
101 |
def swing_tree(swing_node: Markup_Node => DefaultMutableTreeNode): DefaultMutableTreeNode = |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
102 |
{ |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
103 |
def swing(tree: Markup_Tree): DefaultMutableTreeNode = |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
104 |
{ |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
105 |
val node = swing_node(tree.node) |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
106 |
tree.branches foreach ((branch: Markup_Tree) => node.add(swing(branch))) |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
107 |
node |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
108 |
} |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
109 |
swing(root) |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
110 |
} |
34393 | 111 |
} |