author | wenzelm |
Wed, 18 Aug 2010 23:44:50 +0200 | |
changeset 38479 | e628da370072 |
parent 38478 | src/Pure/PIDE/markup_node.scala@7766812a01e7 |
child 38482 | 7b6ee937b75f |
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) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
21 |
|
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
22 |
|
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
23 |
/* 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
|
24 |
|
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
25 |
object Branches |
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 |
type Entry = (Node, Markup_Tree) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
28 |
type T = SortedMap[Node, Entry] |
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 |
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
|
31 |
{ |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
32 |
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
|
33 |
}) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
34 |
def update(branches: T, entries: Entry*): T = |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
35 |
branches ++ entries.map(e => (e._1 -> e)) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
36 |
def make(entries: List[Entry]): T = update(empty, entries:_*) |
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 |
|
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
39 |
val empty = new Markup_Tree(Branches.empty) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
40 |
} |
34554
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34517
diff
changeset
|
41 |
|
34393 | 42 |
|
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
43 |
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
|
44 |
{ |
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
45 |
import Markup_Tree._ |
34557 | 46 |
|
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
47 |
def + (new_node: Node): Markup_Tree = |
34703 | 48 |
{ |
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
49 |
// FIXME tune overlapping == branches && rest.isEmpty |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
50 |
val (overlapping, rest) = |
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 |
val overlapping = new mutable.ListBuffer[Branches.Entry] |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
53 |
var rest = branches |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
54 |
while (rest.isDefinedAt(new_node)) { |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
55 |
overlapping += rest(new_node) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
56 |
rest -= new_node |
34703 | 57 |
} |
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
58 |
(overlapping.toList, rest) |
34703 | 59 |
} |
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
60 |
overlapping match { |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
61 |
case Nil => |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
62 |
new Markup_Tree(Branches.update(branches, new_node -> empty)) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
63 |
|
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
64 |
case List((node, subtree)) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
65 |
if node.range != new_node.range && (node.range contains new_node.range) => |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
66 |
new Markup_Tree(Branches.update(branches, node -> (subtree + new_node))) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
67 |
|
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
68 |
case _ if overlapping.forall(e => new_node.range contains e._1.range) => |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
69 |
val new_tree = new Markup_Tree(Branches.make(overlapping)) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
70 |
new Markup_Tree(Branches.update(rest, new_node -> new_tree)) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
71 |
|
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
72 |
case _ => // FIXME split markup!? |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
73 |
System.err.println("Ignored overlapping markup: " + new_node); this |
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 |
|
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
104 |
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
|
105 |
{ |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
106 |
for ((_, (node, subtree)) <- branches) { |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
107 |
val current = swing_node(node) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
108 |
subtree.swing_tree(current)(swing_node) |
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38478
diff
changeset
|
109 |
parent.add(current) |
34514
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
110 |
} |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
111 |
} |
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
112 |
} |
34514
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
113 |