author  wenzelm 
Fri, 11 Nov 2011 15:25:22 +0100  
changeset 45456  9ba615ac75fb 
parent 45455  4f974c0c5c2f 
child 45457  615ba724b269 
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 

43520
cec9b95fa35d
explicit import java.lang.System to prevent odd scope problems;
wenzelm
parents:
39178
diff
changeset

10 
import java.lang.System 
34701
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 

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

15 

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

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

17 
{ 
45456  18 
type Select[A] = PartialFunction[Text.Markup, A] 
19 

20 
val empty: Markup_Tree = new Markup_Tree(Branches.empty) 

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

21 

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

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

23 
{ 
45455  24 
type Entry = (Text.Markup, Markup_Tree) 
38578  25 
type T = SortedMap[Text.Range, Entry] 
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

26 

45456  27 
val empty: T = SortedMap.empty(Text.Range.Ordering) 
38562  28 

38578  29 
def update(branches: T, entry: Entry): T = branches + (entry._1.range > entry) 
38657  30 
def single(entry: Entry): T = update(empty, entry) 
38562  31 

38659
afac51977705
Markup_Tree.select: more straightforward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents:
38657
diff
changeset

32 
def overlapping(range: Text.Range, branches: T): T = // FIXME special cases!? 
38566
8176107637ce
Branches.overlapping: proper treatment of stop_range that overlaps with end;
wenzelm
parents:
38564
diff
changeset

33 
{ 
38578  34 
val start = Text.Range(range.start) 
35 
val stop = Text.Range(range.stop) 

38659
afac51977705
Markup_Tree.select: more straightforward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents:
38657
diff
changeset

36 
val bs = branches.range(start, stop) 
38566
8176107637ce
Branches.overlapping: proper treatment of stop_range that overlaps with end;
wenzelm
parents:
38564
diff
changeset

37 
branches.get(stop) match { 
38659
afac51977705
Markup_Tree.select: more straightforward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents:
38657
diff
changeset

38 
case Some(end) if range overlaps end._1.range => update(bs, end) 
afac51977705
Markup_Tree.select: more straightforward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents:
38657
diff
changeset

39 
case _ => bs 
38566
8176107637ce
Branches.overlapping: proper treatment of stop_range that overlaps with end;
wenzelm
parents:
38564
diff
changeset

40 
} 
8176107637ce
Branches.overlapping: proper treatment of stop_range that overlaps with end;
wenzelm
parents:
38564
diff
changeset

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

42 
} 
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 

45456  46 
class Markup_Tree private(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 

38563  50 
override def toString = 
51 
branches.toList.map(_._2) match { 

52 
case Nil => "Empty" 

53 
case list => list.mkString("Tree(", ",", ")") 

54 
} 

55 

45455  56 
def + (new_info: Text.Markup): Markup_Tree = 
34703  57 
{ 
38578  58 
val new_range = new_info.range 
59 
branches.get(new_range) match { 

38482
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset

60 
case None => 
38577  61 
new Markup_Tree(Branches.update(branches, new_info > empty)) 
62 
case Some((info, subtree)) => 

38578  63 
val range = info.range 
38661
f1ba2ae8e58a
Markup_Tree.+: new info tends to sink to bottom, where it is prefered by select;
wenzelm
parents:
38659
diff
changeset

64 
if (range.contains(new_range)) 
38577  65 
new Markup_Tree(Branches.update(branches, info > (subtree + new_info))) 
38578  66 
else if (new_range.contains(branches.head._1) && new_range.contains(branches.last._1)) 
38657  67 
new Markup_Tree(Branches.single(new_info > this)) 
38482
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset

68 
else { 
38578  69 
val body = Branches.overlapping(new_range, branches) 
70 
if (body.forall(e => new_range.contains(e._1))) { 

38659
afac51977705
Markup_Tree.select: more straightforward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents:
38657
diff
changeset

71 
val rest = // branches  body, modulo workarounds for Redblack in Scala 2.8.0 
38657  72 
if (body.size > 1) 
73 
(Branches.empty /: branches)((rest, entry) => 

74 
if (body.isDefinedAt(entry._1)) rest else rest + entry) 

75 
else branches 

38577  76 
new Markup_Tree(Branches.update(rest, new_info > new Markup_Tree(body))) 
38482
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset

77 
} 
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset

78 
else { // FIXME split markup!? 
38577  79 
System.err.println("Ignored overlapping markup information: " + new_info) 
38482
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset

80 
this 
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset

81 
} 
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset

82 
} 
34703  83 
} 
84 
} 

85 

38659
afac51977705
Markup_Tree.select: more straightforward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents:
38657
diff
changeset

86 
private def overlapping(range: Text.Range): Stream[(Text.Range, Branches.Entry)] = 
afac51977705
Markup_Tree.select: more straightforward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents:
38657
diff
changeset

87 
Branches.overlapping(range, branches).toStream 
afac51977705
Markup_Tree.select: more straightforward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents:
38657
diff
changeset

88 

39178
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
39177
diff
changeset

89 
def select[A](root_range: Text.Range)(result: Markup_Tree.Select[A]) 
39177
0468964aec11
simplified Markup_Tree.select: Stream instead of Iterator (again), explicit Option instead of default;
wenzelm
parents:
38845
diff
changeset

90 
: Stream[Text.Info[Option[A]]] = 
38486
f5bbfc019937
Markup_Tree.select: crude version of streambased filtering;
wenzelm
parents:
38482
diff
changeset

91 
{ 
39177
0468964aec11
simplified Markup_Tree.select: Stream instead of Iterator (again), explicit Option instead of default;
wenzelm
parents:
38845
diff
changeset

92 
def stream( 
0468964aec11
simplified Markup_Tree.select: Stream instead of Iterator (again), explicit Option instead of default;
wenzelm
parents:
38845
diff
changeset

93 
last: Text.Offset, 
0468964aec11
simplified Markup_Tree.select: Stream instead of Iterator (again), explicit Option instead of default;
wenzelm
parents:
38845
diff
changeset

94 
stack: List[(Text.Info[Option[A]], Stream[(Text.Range, Branches.Entry)])]) 
0468964aec11
simplified Markup_Tree.select: Stream instead of Iterator (again), explicit Option instead of default;
wenzelm
parents:
38845
diff
changeset

95 
: Stream[Text.Info[Option[A]]] = 
38486
f5bbfc019937
Markup_Tree.select: crude version of streambased filtering;
wenzelm
parents:
38482
diff
changeset

96 
{ 
38659
afac51977705
Markup_Tree.select: more straightforward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents:
38657
diff
changeset

97 
stack match { 
afac51977705
Markup_Tree.select: more straightforward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents:
38657
diff
changeset

98 
case (parent, (range, (info, tree)) #:: more) :: rest => 
afac51977705
Markup_Tree.select: more straightforward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents:
38657
diff
changeset

99 
val subrange = range.restrict(root_range) 
afac51977705
Markup_Tree.select: more straightforward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents:
38657
diff
changeset

100 
val subtree = tree.overlapping(subrange) 
afac51977705
Markup_Tree.select: more straightforward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents:
38657
diff
changeset

101 
val start = subrange.start 
38486
f5bbfc019937
Markup_Tree.select: crude version of streambased filtering;
wenzelm
parents:
38482
diff
changeset

102 

38659
afac51977705
Markup_Tree.select: more straightforward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents:
38657
diff
changeset

103 
if (result.isDefinedAt(info)) { 
39177
0468964aec11
simplified Markup_Tree.select: Stream instead of Iterator (again), explicit Option instead of default;
wenzelm
parents:
38845
diff
changeset

104 
val next = Text.Info[Option[A]](subrange, Some(result(info))) 
38659
afac51977705
Markup_Tree.select: more straightforward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents:
38657
diff
changeset

105 
val nexts = stream(start, (next, subtree) :: (parent, more) :: rest) 
afac51977705
Markup_Tree.select: more straightforward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents:
38657
diff
changeset

106 
if (last < start) parent.restrict(Text.Range(last, start)) #:: nexts 
afac51977705
Markup_Tree.select: more straightforward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents:
38657
diff
changeset

107 
else nexts 
afac51977705
Markup_Tree.select: more straightforward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents:
38657
diff
changeset

108 
} 
afac51977705
Markup_Tree.select: more straightforward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents:
38657
diff
changeset

109 
else stream(last, (parent, subtree #::: more) :: rest) 
afac51977705
Markup_Tree.select: more straightforward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents:
38657
diff
changeset

110 

afac51977705
Markup_Tree.select: more straightforward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents:
38657
diff
changeset

111 
case (parent, Stream.Empty) :: rest => 
afac51977705
Markup_Tree.select: more straightforward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents:
38657
diff
changeset

112 
val stop = parent.range.stop 
afac51977705
Markup_Tree.select: more straightforward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents:
38657
diff
changeset

113 
val nexts = stream(stop, rest) 
afac51977705
Markup_Tree.select: more straightforward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents:
38657
diff
changeset

114 
if (last < stop) parent.restrict(Text.Range(last, stop)) #:: nexts 
afac51977705
Markup_Tree.select: more straightforward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents:
38657
diff
changeset

115 
else nexts 
afac51977705
Markup_Tree.select: more straightforward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents:
38657
diff
changeset

116 

38726
6d5f9af42eca
Markup_Tree.select: uniform treatment of root_range wrt. singularities, yielding empty result stream;
wenzelm
parents:
38661
diff
changeset

117 
case Nil => 
6d5f9af42eca
Markup_Tree.select: uniform treatment of root_range wrt. singularities, yielding empty result stream;
wenzelm
parents:
38661
diff
changeset

118 
val stop = root_range.stop 
39177
0468964aec11
simplified Markup_Tree.select: Stream instead of Iterator (again), explicit Option instead of default;
wenzelm
parents:
38845
diff
changeset

119 
if (last < stop) Stream(Text.Info(Text.Range(last, stop), None)) 
38726
6d5f9af42eca
Markup_Tree.select: uniform treatment of root_range wrt. singularities, yielding empty result stream;
wenzelm
parents:
38661
diff
changeset

120 
else Stream.empty 
38659
afac51977705
Markup_Tree.select: more straightforward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents:
38657
diff
changeset

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

122 
} 
39177
0468964aec11
simplified Markup_Tree.select: Stream instead of Iterator (again), explicit Option instead of default;
wenzelm
parents:
38845
diff
changeset

123 
stream(root_range.start, List((Text.Info(root_range, None), overlapping(root_range)))) 
38486
f5bbfc019937
Markup_Tree.select: crude version of streambased filtering;
wenzelm
parents:
38482
diff
changeset

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

125 

38577  126 
def swing_tree(parent: DefaultMutableTreeNode) 
45455  127 
(swing_node: Text.Markup => DefaultMutableTreeNode) 
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

128 
{ 
38577  129 
for ((_, (info, subtree)) < branches) { 
130 
val current = swing_node(info) 

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

131 
subtree.swing_tree(current)(swing_node) 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

132 
parent.add(current) 
34514
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset

133 
} 
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset

134 
} 
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset

135 
} 
34514
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset

136 