author | wenzelm |
Fri, 20 Aug 2010 22:35:01 +0200 | |
changeset 38571 | f7d7b8054648 |
parent 38568 | f117ba49a59c |
child 38576 | ce3eed2b16f7 |
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 |
{ |
38564 | 20 |
case class Node[A](val range: Text.Range, val info: A) |
38482
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
21 |
{ |
38564 | 22 |
def contains[B](that: Node[B]): Boolean = this.range contains that.range |
23 |
def restrict(r: Text.Range): Node[A] = Node(range.restrict(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 |
|
38566
8176107637ce
Branches.overlapping: proper treatment of stop_range that overlaps with end;
wenzelm
parents:
38564
diff
changeset
|
27 |
/* branches sorted by quasi-order -- overlapping ranges appear as equivalent */ |
38479
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 |
{ |
38564 | 31 |
type Entry = (Node[Any], Markup_Tree) |
32 |
type T = SortedMap[Node[Any], Entry] |
|
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
33 |
|
38564 | 34 |
val empty = SortedMap.empty[Node[Any], Entry](new scala.math.Ordering[Node[Any]] |
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
35 |
{ |
38564 | 36 |
def compare(x: Node[Any], y: Node[Any]): Int = x.range compare y.range |
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
37 |
}) |
38562 | 38 |
|
39 |
def update(branches: T, entry: Entry): T = branches + (entry._1 -> entry) |
|
40 |
||
41 |
def overlapping(range: Text.Range, branches: T): T = |
|
38566
8176107637ce
Branches.overlapping: proper treatment of stop_range that overlaps with end;
wenzelm
parents:
38564
diff
changeset
|
42 |
{ |
38568 | 43 |
val start = Node[Any](Text.Range(range.start), Nil) |
44 |
val stop = Node[Any](Text.Range(range.stop), Nil) |
|
38566
8176107637ce
Branches.overlapping: proper treatment of stop_range that overlaps with end;
wenzelm
parents:
38564
diff
changeset
|
45 |
branches.get(stop) match { |
8176107637ce
Branches.overlapping: proper treatment of stop_range that overlaps with end;
wenzelm
parents:
38564
diff
changeset
|
46 |
case Some(end) if range overlaps end._1.range => |
8176107637ce
Branches.overlapping: proper treatment of stop_range that overlaps with end;
wenzelm
parents:
38564
diff
changeset
|
47 |
update(branches.range(start, stop), end) |
8176107637ce
Branches.overlapping: proper treatment of stop_range that overlaps with end;
wenzelm
parents:
38564
diff
changeset
|
48 |
case _ => branches.range(start, stop) |
8176107637ce
Branches.overlapping: proper treatment of stop_range that overlaps with end;
wenzelm
parents:
38564
diff
changeset
|
49 |
} |
8176107637ce
Branches.overlapping: proper treatment of stop_range that overlaps with end;
wenzelm
parents:
38564
diff
changeset
|
50 |
} |
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
51 |
} |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
52 |
|
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
53 |
val empty = new Markup_Tree(Branches.empty) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
54 |
} |
34554
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34517
diff
changeset
|
55 |
|
34393 | 56 |
|
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
57 |
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
|
58 |
{ |
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
59 |
import Markup_Tree._ |
34557 | 60 |
|
38563 | 61 |
override def toString = |
62 |
branches.toList.map(_._2) match { |
|
63 |
case Nil => "Empty" |
|
64 |
case list => list.mkString("Tree(", ",", ")") |
|
65 |
} |
|
66 |
||
38564 | 67 |
def + (new_node: Node[Any]): Markup_Tree = |
34703 | 68 |
{ |
38482
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
69 |
branches.get(new_node) match { |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
70 |
case None => |
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
71 |
new Markup_Tree(Branches.update(branches, new_node -> empty)) |
38482
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
72 |
case Some((node, subtree)) => |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
73 |
if (node.range != new_node.range && node.contains(new_node)) |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
74 |
new Markup_Tree(Branches.update(branches, node -> (subtree + new_node))) |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
75 |
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
|
76 |
new Markup_Tree(Branches.update(Branches.empty, (new_node -> this))) |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
77 |
else { |
38562 | 78 |
val body = Branches.overlapping(new_node.range, branches) |
79 |
if (body.forall(e => new_node.contains(e._1))) { |
|
80 |
val rest = (branches /: body) { case (bs, (e, _)) => bs - e } |
|
81 |
new Markup_Tree(Branches.update(rest, new_node -> new Markup_Tree(body))) |
|
38482
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
82 |
} |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
83 |
else { // FIXME split markup!? |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
84 |
System.err.println("Ignored overlapping markup: " + new_node) |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
85 |
this |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
86 |
} |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
87 |
} |
34703 | 88 |
} |
89 |
} |
|
90 |
||
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
91 |
// FIXME depth-first with result markup stack |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
92 |
// FIXME projection to given range |
38564 | 93 |
def flatten(parent: Node[Any]): List[Node[Any]] = |
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
94 |
{ |
38564 | 95 |
val result = new mutable.ListBuffer[Node[Any]] |
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
96 |
var offset = parent.range.start |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
97 |
for ((_, (node, subtree)) <- branches.iterator) { |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
98 |
if (offset < node.range.start) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
99 |
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
|
100 |
result ++= subtree.flatten(node) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
101 |
offset = node.range.stop |
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 |
if (offset < parent.range.stop) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
104 |
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
|
105 |
result.toList |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
106 |
} |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
107 |
|
38564 | 108 |
def filter(pred: Node[Any] => Boolean): Markup_Tree = |
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
109 |
{ |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
110 |
val bs = branches.toList.flatMap(entry => { |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
111 |
val (_, (node, subtree)) = entry |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
112 |
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
|
113 |
else subtree.filter(pred).branches.toList |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
114 |
}) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
115 |
new Markup_Tree(Branches.empty ++ bs) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
116 |
} |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
117 |
|
38571
f7d7b8054648
Markup_Tree.select: misc simplification, proper restriction of parent in subtree;
wenzelm
parents:
38568
diff
changeset
|
118 |
def select[A](root: Node[A])(sel: PartialFunction[Any, A]): Stream[Node[A]] = |
38486
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
119 |
{ |
38571
f7d7b8054648
Markup_Tree.select: misc simplification, proper restriction of parent in subtree;
wenzelm
parents:
38568
diff
changeset
|
120 |
def stream(parent: Node[A], bs: Branches.T): Stream[Node[A]] = |
38486
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
121 |
{ |
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
122 |
val substream = |
38562 | 123 |
(for ((_, (node, subtree)) <- Branches.overlapping(parent.range, bs).toStream) yield { |
38564 | 124 |
if (sel.isDefinedAt(node.info)) { |
38571
f7d7b8054648
Markup_Tree.select: misc simplification, proper restriction of parent in subtree;
wenzelm
parents:
38568
diff
changeset
|
125 |
val current = Node(node.range.restrict(parent.range), sel(node.info)) |
38564 | 126 |
stream(current, subtree.branches) |
127 |
} |
|
38571
f7d7b8054648
Markup_Tree.select: misc simplification, proper restriction of parent in subtree;
wenzelm
parents:
38568
diff
changeset
|
128 |
else stream(parent.restrict(node.range), subtree.branches) |
38486
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
129 |
}).flatten |
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
130 |
|
38571
f7d7b8054648
Markup_Tree.select: misc simplification, proper restriction of parent in subtree;
wenzelm
parents:
38568
diff
changeset
|
131 |
def padding(last: Text.Offset, s: Stream[Node[A]]): Stream[Node[A]] = |
38486
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
132 |
s match { |
38562 | 133 |
case (node @ Node(Text.Range(start, stop), _)) #:: rest => |
134 |
if (last < start) |
|
135 |
parent.restrict(Text.Range(last, start)) #:: node #:: padding(stop, rest) |
|
136 |
else node #:: padding(stop, rest) |
|
38564 | 137 |
case Stream.Empty => |
38486
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
138 |
if (last < parent.range.stop) |
38562 | 139 |
Stream(parent.restrict(Text.Range(last, parent.range.stop))) |
38486
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
140 |
else Stream.Empty |
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
141 |
} |
38566
8176107637ce
Branches.overlapping: proper treatment of stop_range that overlaps with end;
wenzelm
parents:
38564
diff
changeset
|
142 |
if (substream.isEmpty) Stream(parent) |
8176107637ce
Branches.overlapping: proper treatment of stop_range that overlaps with end;
wenzelm
parents:
38564
diff
changeset
|
143 |
else padding(parent.range.start, substream) |
38486
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
144 |
} |
38571
f7d7b8054648
Markup_Tree.select: misc simplification, proper restriction of parent in subtree;
wenzelm
parents:
38568
diff
changeset
|
145 |
stream(root, branches) |
38486
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
146 |
} |
f5bbfc019937
Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents:
38482
diff
changeset
|
147 |
|
38564 | 148 |
def swing_tree(parent: DefaultMutableTreeNode)(swing_node: Node[Any] => DefaultMutableTreeNode) |
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
149 |
{ |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
150 |
for ((_, (node, subtree)) <- branches) { |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
151 |
val current = swing_node(node) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
152 |
subtree.swing_tree(current)(swing_node) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
153 |
parent.add(current) |
34514
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
154 |
} |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
155 |
} |
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
156 |
} |
34514
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
157 |