author  wenzelm 
Thu, 19 Aug 2010 17:40:44 +0200  
changeset 38486  f5bbfc019937 
parent 38482  7b6ee937b75f 
child 38562  3de5f0424caa 
permissions  rwrr 
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
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 quasiorder;
wenzelm
parents:
38478
diff
changeset

5 
Markup trees over nested / nonoverlapping 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 quasiorder;
wenzelm
parents:
38478
diff
changeset

13 
import scala.collection.immutable.SortedMap 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

14 
import scala.collection.mutable 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

15 
import scala.annotation.tailrec 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

16 

e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

17 

e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

18 
object Markup_Tree 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

19 
{ 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
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 streambased 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 quasiorder;
wenzelm
parents:
38478
diff
changeset

25 

e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

26 

e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

27 
/* branches sorted by quasiorder  overlapping intervals appear as equivalent */ 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

28 

e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

29 
object Branches 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

30 
{ 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

31 
type Entry = (Node, Markup_Tree) 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

32 
type T = SortedMap[Node, Entry] 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

33 

e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
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 quasiorder;
wenzelm
parents:
38478
diff
changeset

35 
{ 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
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 quasiorder;
wenzelm
parents:
38478
diff
changeset

37 
}) 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

38 
def update(branches: T, entries: Entry*): T = 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

39 
branches ++ entries.map(e => (e._1 > e)) 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

40 
} 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

41 

e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

42 
val empty = new Markup_Tree(Branches.empty) 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

43 
} 
34554
7dc6c231da40
abs. stops, markup nodes depend on docversion;
immler@in.tum.de
parents:
34517
diff
changeset

44 

34393  45 

38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
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 quasiorder;
wenzelm
parents:
38478
diff
changeset

48 
import Markup_Tree._ 
34557  49 

38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
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 quasiorder;
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 quasiorder;
wenzelm
parents:
38478
diff
changeset

77 
// FIXME depthfirst with result markup stack 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

78 
// FIXME projection to given range 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
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 quasiorder;
wenzelm
parents:
38478
diff
changeset

81 
val result = new mutable.ListBuffer[Node] 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

82 
var offset = parent.range.start 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

83 
for ((_, (node, subtree)) < branches.iterator) { 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

84 
if (offset < node.range.start) 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
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 quasiorder;
wenzelm
parents:
38478
diff
changeset

86 
result ++= subtree.flatten(node) 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

87 
offset = node.range.stop 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

88 
} 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

89 
if (offset < parent.range.stop) 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
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 quasiorder;
wenzelm
parents:
38478
diff
changeset

91 
result.toList 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

92 
} 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

93 

e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

94 
def filter(pred: Node => Boolean): Markup_Tree = 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

95 
{ 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

96 
val bs = branches.toList.flatMap(entry => { 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

97 
val (_, (node, subtree)) = entry 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
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 quasiorder;
wenzelm
parents:
38478
diff
changeset

99 
else subtree.filter(pred).branches.toList 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

100 
}) 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

101 
new Markup_Tree(Branches.empty ++ bs) 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

102 
} 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

103 

38486
f5bbfc019937
Markup_Tree.select: crude version of streambased 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 streambased filtering;
wenzelm
parents:
38482
diff
changeset

105 
{ 
f5bbfc019937
Markup_Tree.select: crude version of streambased filtering;
wenzelm
parents:
38482
diff
changeset

106 
def stream(parent: Node, bs: Branches.T): Stream[Node] = 
f5bbfc019937
Markup_Tree.select: crude version of streambased filtering;
wenzelm
parents:
38482
diff
changeset

107 
{ 
f5bbfc019937
Markup_Tree.select: crude version of streambased filtering;
wenzelm
parents:
38482
diff
changeset

108 
val start = Node(parent.range.start_range, Nil) 
f5bbfc019937
Markup_Tree.select: crude version of streambased filtering;
wenzelm
parents:
38482
diff
changeset

109 
val stop = Node(parent.range.stop_range, Nil) 
f5bbfc019937
Markup_Tree.select: crude version of streambased filtering;
wenzelm
parents:
38482
diff
changeset

110 
val substream = 
f5bbfc019937
Markup_Tree.select: crude version of streambased filtering;
wenzelm
parents:
38482
diff
changeset

111 
(for ((_, (node, subtree)) < bs.range(start, stop).toStream) yield { 
f5bbfc019937
Markup_Tree.select: crude version of streambased filtering;
wenzelm
parents:
38482
diff
changeset

112 
if (sel.isDefinedAt(node)) 
f5bbfc019937
Markup_Tree.select: crude version of streambased filtering;
wenzelm
parents:
38482
diff
changeset

113 
stream(node.intersect(parent.range), subtree.branches) 
f5bbfc019937
Markup_Tree.select: crude version of streambased filtering;
wenzelm
parents:
38482
diff
changeset

114 
else stream(parent, subtree.branches) 
f5bbfc019937
Markup_Tree.select: crude version of streambased filtering;
wenzelm
parents:
38482
diff
changeset

115 
}).flatten 
f5bbfc019937
Markup_Tree.select: crude version of streambased filtering;
wenzelm
parents:
38482
diff
changeset

116 

f5bbfc019937
Markup_Tree.select: crude version of streambased filtering;
wenzelm
parents:
38482
diff
changeset

117 
def padding(last: Text.Offset, s: Stream[Node]): Stream[Node] = 
f5bbfc019937
Markup_Tree.select: crude version of streambased filtering;
wenzelm
parents:
38482
diff
changeset

118 
s match { 
f5bbfc019937
Markup_Tree.select: crude version of streambased filtering;
wenzelm
parents:
38482
diff
changeset

119 
case node #:: rest => 
f5bbfc019937
Markup_Tree.select: crude version of streambased filtering;
wenzelm
parents:
38482
diff
changeset

120 
if (last < node.range.start) 
f5bbfc019937
Markup_Tree.select: crude version of streambased filtering;
wenzelm
parents:
38482
diff
changeset

121 
parent.intersect(Text.Range(last, node.range.start)) #:: 
f5bbfc019937
Markup_Tree.select: crude version of streambased filtering;
wenzelm
parents:
38482
diff
changeset

122 
node #:: padding(node.range.stop, rest) 
f5bbfc019937
Markup_Tree.select: crude version of streambased filtering;
wenzelm
parents:
38482
diff
changeset

123 
else node #:: padding(node.range.stop, rest) 
f5bbfc019937
Markup_Tree.select: crude version of streambased filtering;
wenzelm
parents:
38482
diff
changeset

124 
case Stream.Empty => // FIXME 
f5bbfc019937
Markup_Tree.select: crude version of streambased filtering;
wenzelm
parents:
38482
diff
changeset

125 
if (last < parent.range.stop) 
f5bbfc019937
Markup_Tree.select: crude version of streambased filtering;
wenzelm
parents:
38482
diff
changeset

126 
Stream(parent.intersect(Text.Range(last, parent.range.stop))) 
f5bbfc019937
Markup_Tree.select: crude version of streambased filtering;
wenzelm
parents:
38482
diff
changeset

127 
else Stream.Empty 
f5bbfc019937
Markup_Tree.select: crude version of streambased filtering;
wenzelm
parents:
38482
diff
changeset

128 
} 
f5bbfc019937
Markup_Tree.select: crude version of streambased filtering;
wenzelm
parents:
38482
diff
changeset

129 
padding(parent.range.start, substream) 
f5bbfc019937
Markup_Tree.select: crude version of streambased filtering;
wenzelm
parents:
38482
diff
changeset

130 
} 
f5bbfc019937
Markup_Tree.select: crude version of streambased filtering;
wenzelm
parents:
38482
diff
changeset

131 
// FIXME handle disjoint range!? 
f5bbfc019937
Markup_Tree.select: crude version of streambased filtering;
wenzelm
parents:
38482
diff
changeset

132 
stream(Node(range, Nil), branches) 
f5bbfc019937
Markup_Tree.select: crude version of streambased filtering;
wenzelm
parents:
38482
diff
changeset

133 
} 
f5bbfc019937
Markup_Tree.select: crude version of streambased filtering;
wenzelm
parents:
38482
diff
changeset

134 

38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
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 quasiorder;
wenzelm
parents:
38478
diff
changeset

136 
{ 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

137 
for ((_, (node, subtree)) < branches) { 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

138 
val current = swing_node(node) 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

139 
subtree.swing_tree(current)(swing_node) 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
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 