author | wenzelm |
Thu, 19 Aug 2010 12:41:40 +0200 | |
changeset 38482 | 7b6ee937b75f |
parent 38479 | e628da370072 |
child 38486 | f5bbfc019937 |
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 |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
23 |
} |
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
24 |
|
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 |
/* 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
|
27 |
|
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
28 |
object Branches |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
29 |
{ |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
30 |
type Entry = (Node, Markup_Tree) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
31 |
type T = SortedMap[Node, Entry] |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
32 |
|
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
33 |
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
|
34 |
{ |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
35 |
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
|
36 |
}) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
37 |
def update(branches: T, entries: Entry*): T = |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
38 |
branches ++ entries.map(e => (e._1 -> e)) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
39 |
} |
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 |
val empty = new Markup_Tree(Branches.empty) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
42 |
} |
34554
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34517
diff
changeset
|
43 |
|
34393 | 44 |
|
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
45 |
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
|
46 |
{ |
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
47 |
import Markup_Tree._ |
34557 | 48 |
|
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
49 |
def + (new_node: Node): Markup_Tree = |
34703 | 50 |
{ |
38482
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
51 |
branches.get(new_node) match { |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
52 |
case None => |
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
53 |
new Markup_Tree(Branches.update(branches, new_node -> empty)) |
38482
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
54 |
case Some((node, subtree)) => |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
55 |
if (node.range != new_node.range && node.contains(new_node)) |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
56 |
new Markup_Tree(Branches.update(branches, node -> (subtree + new_node))) |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
57 |
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
|
58 |
new Markup_Tree(Branches.update(Branches.empty, (new_node -> this))) |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
59 |
else { |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
60 |
var overlapping = Branches.empty |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
61 |
var rest = branches |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
62 |
while (rest.isDefinedAt(new_node)) { |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
63 |
overlapping = Branches.update(overlapping, rest(new_node)) |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
64 |
rest -= new_node |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
65 |
} |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
66 |
if (overlapping.forall(e => new_node.contains(e._1))) |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
67 |
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
|
68 |
else { // FIXME split markup!? |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
69 |
System.err.println("Ignored overlapping markup: " + new_node) |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
70 |
this |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
71 |
} |
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset
|
72 |
} |
34703 | 73 |
} |
74 |
} |
|
75 |
||
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
76 |
// FIXME depth-first with result markup stack |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
77 |
// FIXME projection to given range |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
78 |
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
|
79 |
{ |
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
80 |
val result = new mutable.ListBuffer[Node] |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
81 |
var offset = parent.range.start |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
82 |
for ((_, (node, subtree)) <- branches.iterator) { |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
83 |
if (offset < node.range.start) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
84 |
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
|
85 |
result ++= subtree.flatten(node) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
86 |
offset = node.range.stop |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
87 |
} |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
88 |
if (offset < parent.range.stop) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
89 |
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
|
90 |
result.toList |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
91 |
} |
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 |
def filter(pred: Node => Boolean): Markup_Tree = |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
94 |
{ |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
95 |
val bs = branches.toList.flatMap(entry => { |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
96 |
val (_, (node, subtree)) = entry |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
97 |
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
|
98 |
else subtree.filter(pred).branches.toList |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
99 |
}) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
100 |
new Markup_Tree(Branches.empty ++ bs) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
101 |
} |
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 |
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
|
104 |
{ |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
105 |
for ((_, (node, subtree)) <- branches) { |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
106 |
val current = swing_node(node) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
107 |
subtree.swing_tree(current)(swing_node) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
108 |
parent.add(current) |
34514
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
109 |
} |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
110 |
} |
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
111 |
} |
34514
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
112 |