author | wenzelm |
Thu, 19 Aug 2010 17:40:44 +0200 | |
changeset 38486 | f5bbfc019937 |
parent 38482 | 7b6ee937b75f |
child 38562 | 3de5f0424caa |
permissions | -rw-r--r-- |
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
1 |
/* Title: Pure/PIDE/markup_tree.scala |
36676 | 2 |
Author: Fabian Immler, TU Munich |
3 |
Author: Makarius |
|
4 |
||
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
5 |
Markup trees over nested / non-overlapping text ranges. |
36676 | 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 |
|
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
13 |
import scala.collection.immutable.SortedMap |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
14 |
import scala.collection.mutable |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
15 |
import scala.annotation.tailrec |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
16 |
|
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
17 |
|
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
18 |
object Markup_Tree |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
19 |
{ |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
20 |
case class Node(val range: Text.Range, val info: Any) |
38482
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
21 |
{ |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
22 |
def contains(that: Node): Boolean = this.range contains that.range |
38486
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
23 |
def intersect(r: Text.Range): Node = Node(range.intersect(r), info) |
38482
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
24 |
} |
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
25 |
|
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
26 |
|
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
27 |
/* branches sorted by quasi-order -- overlapping intervals appear as equivalent */ |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
28 |
|
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
29 |
object Branches |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
30 |
{ |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
31 |
type Entry = (Node, Markup_Tree) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
32 |
type T = SortedMap[Node, Entry] |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
33 |
|
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
34 |
val empty = SortedMap.empty[Node, Entry](new scala.math.Ordering[Node] |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
35 |
{ |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
36 |
def compare(x: Node, y: Node): Int = x.range compare y.range |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
37 |
}) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
38 |
def update(branches: T, entries: Entry*): T = |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
39 |
branches ++ entries.map(e => (e._1 -> e)) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
40 |
} |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
41 |
|
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
42 |
val empty = new Markup_Tree(Branches.empty) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
43 |
} |
34554
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34517
diff
changeset
|
44 |
|
34393 | 45 |
|
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
46 |
case class Markup_Tree(val branches: Markup_Tree.Branches.T) |
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
47 |
{ |
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
48 |
import Markup_Tree._ |
34557 | 49 |
|
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
50 |
def + (new_node: Node): Markup_Tree = |
34703 | 51 |
{ |
38482
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
52 |
branches.get(new_node) match { |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
53 |
case None => |
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
54 |
new Markup_Tree(Branches.update(branches, new_node -> empty)) |
38482
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
55 |
case Some((node, subtree)) => |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
56 |
if (node.range != new_node.range && node.contains(new_node)) |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
57 |
new Markup_Tree(Branches.update(branches, node -> (subtree + new_node))) |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
58 |
else if (new_node.contains(branches.head._1) && new_node.contains(branches.last._1)) |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
59 |
new Markup_Tree(Branches.update(Branches.empty, (new_node -> this))) |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
60 |
else { |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
61 |
var overlapping = Branches.empty |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
62 |
var rest = branches |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
63 |
while (rest.isDefinedAt(new_node)) { |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
64 |
overlapping = Branches.update(overlapping, rest(new_node)) |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
65 |
rest -= new_node |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
66 |
} |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
67 |
if (overlapping.forall(e => new_node.contains(e._1))) |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
68 |
new Markup_Tree(Branches.update(rest, new_node -> new Markup_Tree(overlapping))) |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
69 |
else { // FIXME split markup!? |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
70 |
System.err.println("Ignored overlapping markup: " + new_node) |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
71 |
this |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
72 |
} |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
73 |
} |
34703 | 74 |
} |
75 |
} |
|
76 |
||
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
77 |
// FIXME depth-first with result markup stack |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
78 |
// FIXME projection to given range |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
79 |
def flatten(parent: Node): List[Node] = |
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
80 |
{ |
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
81 |
val result = new mutable.ListBuffer[Node] |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
82 |
var offset = parent.range.start |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
83 |
for ((_, (node, subtree)) <- branches.iterator) { |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
84 |
if (offset < node.range.start) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
85 |
result += new Node(Text.Range(offset, node.range.start), parent.info) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
86 |
result ++= subtree.flatten(node) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
87 |
offset = node.range.stop |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
88 |
} |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
89 |
if (offset < parent.range.stop) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
90 |
result += new Node(Text.Range(offset, parent.range.stop), parent.info) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
91 |
result.toList |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
92 |
} |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
93 |
|
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
94 |
def filter(pred: Node => Boolean): Markup_Tree = |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
95 |
{ |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
96 |
val bs = branches.toList.flatMap(entry => { |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
97 |
val (_, (node, subtree)) = entry |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
98 |
if (pred(node)) List((node, (node, subtree.filter(pred)))) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
99 |
else subtree.filter(pred).branches.toList |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
100 |
}) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
101 |
new Markup_Tree(Branches.empty ++ bs) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
102 |
} |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
103 |
|
38486
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
104 |
def select[A](range: Text.Range)(sel: PartialFunction[Node, A]): Stream[Node] = |
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
105 |
{ |
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
106 |
def stream(parent: Node, bs: Branches.T): Stream[Node] = |
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
107 |
{ |
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
108 |
val start = Node(parent.range.start_range, Nil) |
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
109 |
val stop = Node(parent.range.stop_range, Nil) |
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
110 |
val substream = |
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
111 |
(for ((_, (node, subtree)) <- bs.range(start, stop).toStream) yield { |
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
112 |
if (sel.isDefinedAt(node)) |
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
113 |
stream(node.intersect(parent.range), subtree.branches) |
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
114 |
else stream(parent, subtree.branches) |
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
115 |
}).flatten |
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
116 |
|
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
117 |
def padding(last: Text.Offset, s: Stream[Node]): Stream[Node] = |
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
118 |
s match { |
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
119 |
case node #:: rest => |
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
120 |
if (last < node.range.start) |
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
121 |
parent.intersect(Text.Range(last, node.range.start)) #:: |
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
122 |
node #:: padding(node.range.stop, rest) |
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
123 |
else node #:: padding(node.range.stop, rest) |
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
124 |
case Stream.Empty => // FIXME |
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
125 |
if (last < parent.range.stop) |
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
126 |
Stream(parent.intersect(Text.Range(last, parent.range.stop))) |
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
127 |
else Stream.Empty |
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
128 |
} |
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
129 |
padding(parent.range.start, substream) |
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
130 |
} |
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
131 |
// FIXME handle disjoint range!? |
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
132 |
stream(Node(range, Nil), branches) |
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
133 |
} |
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
134 |
|
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
135 |
def swing_tree(parent: DefaultMutableTreeNode)(swing_node: Node => DefaultMutableTreeNode) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
136 |
{ |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
137 |
for ((_, (node, subtree)) <- branches) { |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
138 |
val current = swing_node(node) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
139 |
subtree.swing_tree(current)(swing_node) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
140 |
parent.add(current) |
34514
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
141 |
} |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
142 |
} |
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
143 |
} |
34514
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
144 |