author  wenzelm 
Thu, 27 Mar 2014 12:11:32 +0100  
changeset 56301  1da7b4c33db9 
parent 56300  8346b664fa7a 
child 56302  c63ab5263008 
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 
45673
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
wenzelm
parents:
45667
diff
changeset

2 
Module: PIDE 
36676  3 
Author: Fabian Immler, TU Munich 
4 
Author: Makarius 

5 

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

6 
Markup trees over nested / nonoverlapping text ranges. 
36676  7 
*/ 
34393  8 

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

9 
package isabelle 
34393  10 

34701
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34676
diff
changeset

11 

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

12 
import scala.collection.immutable.SortedMap 
49614  13 
import scala.collection.mutable 
49467  14 
import scala.annotation.tailrec 
38479
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 

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

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

18 
{ 
50551  19 
/* construct trees */ 
20 

45456  21 
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

22 

56301
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

23 
def merge(trees: List[Markup_Tree], range: Text.Range, elements: Document.Elements): Markup_Tree = 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

24 
(empty /: trees)(_.merge(_, range, elements)) 
56299
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
55820
diff
changeset

25 

49467  26 
def merge_disjoint(trees: List[Markup_Tree]): Markup_Tree = 
27 
trees match { 

28 
case Nil => empty 

29 
case head :: tail => 

30 
new Markup_Tree( 

31 
(head.branches /: tail) { 

32 
case (branches, tree) => 

33 
(branches /: tree.branches) { 

34 
case (bs, (r, entry)) => 

35 
require(!bs.isDefinedAt(r)) 

36 
bs + (r > entry) 

37 
} 

38 
}) 

39 
} 

40 

50551  41 

42 
/* tree building blocks */ 

43 

45473  44 
object Entry 
45 
{ 

46 
def apply(markup: Text.Markup, subtree: Markup_Tree): Entry = 

55652
33ad12ef79ff
eliminated somewhat pointless elements index (see also f793dd5d84b2, 2b7fed8c9c4ac): less memory and more speed (avoid linear "exists" of 19dffae33cde);
wenzelm
parents:
55645
diff
changeset

47 
Entry(markup.range, List(markup.info), subtree) 
45473  48 
} 
49 

45474
f793dd5d84b2
index markup elements for more efficient cumulate/select operations;
wenzelm
parents:
45473
diff
changeset

50 
sealed case class Entry( 
f793dd5d84b2
index markup elements for more efficient cumulate/select operations;
wenzelm
parents:
45473
diff
changeset

51 
range: Text.Range, 
f793dd5d84b2
index markup elements for more efficient cumulate/select operations;
wenzelm
parents:
45473
diff
changeset

52 
rev_markup: List[XML.Elem], 
55652
33ad12ef79ff
eliminated somewhat pointless elements index (see also f793dd5d84b2, 2b7fed8c9c4ac): less memory and more speed (avoid linear "exists" of 19dffae33cde);
wenzelm
parents:
55645
diff
changeset

53 
subtree: Markup_Tree) 
45469
25306d92f4ad
refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents:
45468
diff
changeset

54 
{ 
50552
2b7fd8c9c4ac
maintain subtree_elements for improved performance of cumulate operator;
wenzelm
parents:
50551
diff
changeset

55 
def markup: List[XML.Elem] = rev_markup.reverse 
45474
f793dd5d84b2
index markup elements for more efficient cumulate/select operations;
wenzelm
parents:
45473
diff
changeset

56 

55820
61869776ce1f
tuned signature  more explicit Document.Elements;
wenzelm
parents:
55652
diff
changeset

57 
def filter_markup(elements: Document.Elements): List[XML.Elem] = 
55645
561754277494
tuned  remaining rev_markup is rather short after filter;
wenzelm
parents:
55622
diff
changeset

58 
{ 
561754277494
tuned  remaining rev_markup is rather short after filter;
wenzelm
parents:
55622
diff
changeset

59 
var result: List[XML.Elem] = Nil 
55820
61869776ce1f
tuned signature  more explicit Document.Elements;
wenzelm
parents:
55652
diff
changeset

60 
for { elem < rev_markup; if (elements(elem.name)) } 
55645
561754277494
tuned  remaining rev_markup is rather short after filter;
wenzelm
parents:
55622
diff
changeset

61 
result ::= elem 
561754277494
tuned  remaining rev_markup is rather short after filter;
wenzelm
parents:
55622
diff
changeset

62 
result.toList 
561754277494
tuned  remaining rev_markup is rather short after filter;
wenzelm
parents:
55622
diff
changeset

63 
} 
561754277494
tuned  remaining rev_markup is rather short after filter;
wenzelm
parents:
55622
diff
changeset

64 

55652
33ad12ef79ff
eliminated somewhat pointless elements index (see also f793dd5d84b2, 2b7fed8c9c4ac): less memory and more speed (avoid linear "exists" of 19dffae33cde);
wenzelm
parents:
55645
diff
changeset

65 
def + (markup: Text.Markup): Entry = copy(rev_markup = markup.info :: rev_markup) 
33ad12ef79ff
eliminated somewhat pointless elements index (see also f793dd5d84b2, 2b7fed8c9c4ac): less memory and more speed (avoid linear "exists" of 19dffae33cde);
wenzelm
parents:
55645
diff
changeset

66 
def \ (markup: Text.Markup): Entry = copy(subtree = subtree + markup) 
45469
25306d92f4ad
refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents:
45468
diff
changeset

67 
} 
25306d92f4ad
refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents:
45468
diff
changeset

68 

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

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

70 
{ 
38578  71 
type T = SortedMap[Text.Range, Entry] 
45456  72 
val empty: T = SortedMap.empty(Text.Range.Ordering) 
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

73 
} 
49466  74 

75 

76 
/* XML representation */ 

77 

49650
9fad6480300d
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents:
49614
diff
changeset

78 
@tailrec private def strip_elems( 
9fad6480300d
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents:
49614
diff
changeset

79 
elems: List[XML.Elem], body: XML.Body): (List[XML.Elem], XML.Body) = 
49467  80 
body match { 
49650
9fad6480300d
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents:
49614
diff
changeset

81 
case List(XML.Wrapped_Elem(markup1, body1, body2)) => 
9fad6480300d
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents:
49614
diff
changeset

82 
strip_elems(XML.Elem(markup1, body1) :: elems, body2) 
9fad6480300d
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents:
49614
diff
changeset

83 
case List(XML.Elem(markup1, body1)) => 
9fad6480300d
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents:
49614
diff
changeset

84 
strip_elems(XML.Elem(markup1, Nil) :: elems, body1) 
9fad6480300d
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents:
49614
diff
changeset

85 
case _ => (elems, body) 
49467  86 
} 
87 

88 
private def make_trees(acc: (Int, List[Markup_Tree]), tree: XML.Tree): (Int, List[Markup_Tree]) = 

89 
{ 

90 
val (offset, markup_trees) = acc 

91 

92 
strip_elems(Nil, List(tree)) match { 

93 
case (Nil, body) => 

94 
(offset + XML.text_length(body), markup_trees) 

49466  95 

49469  96 
case (elems, body) => 
97 
val (end_offset, subtrees) = ((offset, Nil: List[Markup_Tree]) /: body)(make_trees) 

50642
aca12f646772
ignore markup elements over empty body, which are not welldefined within markup tree and fail to work with merge_disjoint (e.g. multiple inlined positions);
wenzelm
parents:
50552
diff
changeset

98 
if (offset == end_offset) acc 
aca12f646772
ignore markup elements over empty body, which are not welldefined within markup tree and fail to work with merge_disjoint (e.g. multiple inlined positions);
wenzelm
parents:
50552
diff
changeset

99 
else { 
aca12f646772
ignore markup elements over empty body, which are not welldefined within markup tree and fail to work with merge_disjoint (e.g. multiple inlined positions);
wenzelm
parents:
50552
diff
changeset

100 
val range = Text.Range(offset, end_offset) 
aca12f646772
ignore markup elements over empty body, which are not welldefined within markup tree and fail to work with merge_disjoint (e.g. multiple inlined positions);
wenzelm
parents:
50552
diff
changeset

101 
val entry = Entry(range, elems, merge_disjoint(subtrees)) 
aca12f646772
ignore markup elements over empty body, which are not welldefined within markup tree and fail to work with merge_disjoint (e.g. multiple inlined positions);
wenzelm
parents:
50552
diff
changeset

102 
(end_offset, new Markup_Tree(Branches.empty, entry) :: markup_trees) 
aca12f646772
ignore markup elements over empty body, which are not welldefined within markup tree and fail to work with merge_disjoint (e.g. multiple inlined positions);
wenzelm
parents:
50552
diff
changeset

103 
} 
49466  104 
} 
49467  105 
} 
49466  106 

49467  107 
def from_XML(body: XML.Body): Markup_Tree = 
108 
merge_disjoint(((0, Nil: List[Markup_Tree]) /: body)(make_trees)._2) 

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

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

110 

34393  111 

51618
a3577cd80c41
tuned signature  avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
wenzelm
parents:
50642
diff
changeset

112 
final class Markup_Tree private(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

113 
{ 
49417  114 
import Markup_Tree._ 
115 

45469
25306d92f4ad
refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents:
45468
diff
changeset

116 
private def this(branches: Markup_Tree.Branches.T, entry: Markup_Tree.Entry) = 
25306d92f4ad
refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents:
45468
diff
changeset

117 
this(branches + (entry.range > entry)) 
25306d92f4ad
refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents:
45468
diff
changeset

118 

25306d92f4ad
refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents:
45468
diff
changeset

119 
private def overlapping(range: Text.Range): Branches.T = 
45457  120 
{ 
121 
val start = Text.Range(range.start) 

122 
val stop = Text.Range(range.stop) 

123 
val bs = branches.range(start, stop) 

124 
branches.get(stop) match { 

45469
25306d92f4ad
refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents:
45468
diff
changeset

125 
case Some(end) if range overlaps end.range => bs + (end.range > end) 
45457  126 
case _ => bs 
127 
} 

128 
} 

129 

45469
25306d92f4ad
refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents:
45468
diff
changeset

130 
def + (new_markup: Text.Markup): Markup_Tree = 
34703  131 
{ 
45469
25306d92f4ad
refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents:
45468
diff
changeset

132 
val new_range = new_markup.range 
25306d92f4ad
refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents:
45468
diff
changeset

133 

38578  134 
branches.get(new_range) match { 
45473  135 
case None => new Markup_Tree(branches, Entry(new_markup, empty)) 
45469
25306d92f4ad
refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents:
45468
diff
changeset

136 
case Some(entry) => 
25306d92f4ad
refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents:
45468
diff
changeset

137 
if (entry.range == new_range) 
50552
2b7fd8c9c4ac
maintain subtree_elements for improved performance of cumulate operator;
wenzelm
parents:
50551
diff
changeset

138 
new Markup_Tree(branches, entry + new_markup) 
45469
25306d92f4ad
refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents:
45468
diff
changeset

139 
else if (entry.range.contains(new_range)) 
50552
2b7fd8c9c4ac
maintain subtree_elements for improved performance of cumulate operator;
wenzelm
parents:
50551
diff
changeset

140 
new Markup_Tree(branches, entry \ new_markup) 
38578  141 
else if (new_range.contains(branches.head._1) && new_range.contains(branches.last._1)) 
45473  142 
new Markup_Tree(Branches.empty, Entry(new_markup, this)) 
38482
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset

143 
else { 
45457  144 
val body = overlapping(new_range) 
49607
b610c0d52bfa
updated to consolidated SortedMap in scala2.9.x;
wenzelm
parents:
49469
diff
changeset

145 
if (body.forall(e => new_range.contains(e._1))) 
b610c0d52bfa
updated to consolidated SortedMap in scala2.9.x;
wenzelm
parents:
49469
diff
changeset

146 
new Markup_Tree(branches  body.keys, Entry(new_markup, new Markup_Tree(body))) 
49608  147 
else { 
55618  148 
System.err.println("Ignored overlapping markup information: " + new_markup + 
48762  149 
body.filter(e => !new_range.contains(e._1)).mkString("\n")) 
38482
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset

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

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

152 
} 
34703  153 
} 
154 
} 

155 

56301
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

156 
def merge(other: Markup_Tree, root_range: Text.Range, elements: Document.Elements): Markup_Tree = 
49614  157 
{ 
56301
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

158 
def merge_trees(tree1: Markup_Tree, tree2: Markup_Tree): Markup_Tree = 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

159 
if (tree1 eq tree2) tree1 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

160 
else if (tree1.branches.isEmpty) tree2 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

161 
else 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

162 
(tree1 /: tree2.branches)( 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

163 
{ case (tree, (range, entry)) => 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

164 
if (range overlaps root_range) { 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

165 
(merge_trees(tree, entry.subtree) /: entry.filter_markup(elements))( 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

166 
{ case (t, elem) => t + Text.Info(range, elem) }) 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

167 
} 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

168 
else tree 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

169 
}) 
49614  170 

56301
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

171 
merge_trees(this, other) 
49614  172 
} 
173 

55820
61869776ce1f
tuned signature  more explicit Document.Elements;
wenzelm
parents:
55652
diff
changeset

174 
def cumulate[A](root_range: Text.Range, root_info: A, elements: Document.Elements, 
52900
d29bf6db8a2d
more elementary list structures for markup tree traversal;
wenzelm
parents:
52889
diff
changeset

175 
result: (A, Text.Markup) => Option[A]): List[Text.Info[A]] = 
45459  176 
{ 
46178
1c5c88f6feb5
clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents:
46165
diff
changeset

177 
def results(x: A, entry: Entry): Option[A] = 
50552
2b7fd8c9c4ac
maintain subtree_elements for improved performance of cumulate operator;
wenzelm
parents:
50551
diff
changeset

178 
{ 
52889
ea3338812e67
more tight interface for markup cumulate/select: avoid duplicate application, allow to defer decision about definedness;
wenzelm
parents:
52642
diff
changeset

179 
var y = x 
ea3338812e67
more tight interface for markup cumulate/select: avoid duplicate application, allow to defer decision about definedness;
wenzelm
parents:
52642
diff
changeset

180 
var changed = false 
ea3338812e67
more tight interface for markup cumulate/select: avoid duplicate application, allow to defer decision about definedness;
wenzelm
parents:
52642
diff
changeset

181 
for { 
55645
561754277494
tuned  remaining rev_markup is rather short after filter;
wenzelm
parents:
55622
diff
changeset

182 
elem < entry.filter_markup(elements) 
55620  183 
y1 < result(y, Text.Info(entry.range, elem)) 
52889
ea3338812e67
more tight interface for markup cumulate/select: avoid duplicate application, allow to defer decision about definedness;
wenzelm
parents:
52642
diff
changeset

184 
} { y = y1; changed = true } 
50552
2b7fd8c9c4ac
maintain subtree_elements for improved performance of cumulate operator;
wenzelm
parents:
50551
diff
changeset

185 
if (changed) Some(y) else None 
2b7fd8c9c4ac
maintain subtree_elements for improved performance of cumulate operator;
wenzelm
parents:
50551
diff
changeset

186 
} 
45467  187 

52900
d29bf6db8a2d
more elementary list structures for markup tree traversal;
wenzelm
parents:
52889
diff
changeset

188 
def traverse( 
45459  189 
last: Text.Offset, 
52900
d29bf6db8a2d
more elementary list structures for markup tree traversal;
wenzelm
parents:
52889
diff
changeset

190 
stack: List[(Text.Info[A], List[(Text.Range, Entry)])]): List[Text.Info[A]] = 
45459  191 
{ 
192 
stack match { 

52900
d29bf6db8a2d
more elementary list structures for markup tree traversal;
wenzelm
parents:
52889
diff
changeset

193 
case (parent, (range, entry) :: more) :: rest => 
45467  194 
val subrange = range.restrict(root_range) 
55652
33ad12ef79ff
eliminated somewhat pointless elements index (see also f793dd5d84b2, 2b7fed8c9c4ac): less memory and more speed (avoid linear "exists" of 19dffae33cde);
wenzelm
parents:
55645
diff
changeset

195 
val subtree = entry.subtree.overlapping(subrange).toList 
45459  196 
val start = subrange.start 
197 

55652
33ad12ef79ff
eliminated somewhat pointless elements index (see also f793dd5d84b2, 2b7fed8c9c4ac): less memory and more speed (avoid linear "exists" of 19dffae33cde);
wenzelm
parents:
55645
diff
changeset

198 
results(parent.info, entry) match { 
45469
25306d92f4ad
refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents:
45468
diff
changeset

199 
case Some(res) => 
25306d92f4ad
refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents:
45468
diff
changeset

200 
val next = Text.Info(subrange, res) 
52900
d29bf6db8a2d
more elementary list structures for markup tree traversal;
wenzelm
parents:
52889
diff
changeset

201 
val nexts = traverse(start, (next, subtree) :: (parent, more) :: rest) 
d29bf6db8a2d
more elementary list structures for markup tree traversal;
wenzelm
parents:
52889
diff
changeset

202 
if (last < start) parent.restrict(Text.Range(last, start)) :: nexts 
45469
25306d92f4ad
refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents:
45468
diff
changeset

203 
else nexts 
52900
d29bf6db8a2d
more elementary list structures for markup tree traversal;
wenzelm
parents:
52889
diff
changeset

204 
case None => traverse(last, (parent, subtree ::: more) :: rest) 
45459  205 
} 
206 

52900
d29bf6db8a2d
more elementary list structures for markup tree traversal;
wenzelm
parents:
52889
diff
changeset

207 
case (parent, Nil) :: rest => 
45459  208 
val stop = parent.range.stop 
52900
d29bf6db8a2d
more elementary list structures for markup tree traversal;
wenzelm
parents:
52889
diff
changeset

209 
val nexts = traverse(stop, rest) 
d29bf6db8a2d
more elementary list structures for markup tree traversal;
wenzelm
parents:
52889
diff
changeset

210 
if (last < stop) parent.restrict(Text.Range(last, stop)) :: nexts 
45459  211 
else nexts 
212 

213 
case Nil => 

45467  214 
val stop = root_range.stop 
52900
d29bf6db8a2d
more elementary list structures for markup tree traversal;
wenzelm
parents:
52889
diff
changeset

215 
if (last < stop) List(Text.Info(Text.Range(last, stop), root_info)) 
d29bf6db8a2d
more elementary list structures for markup tree traversal;
wenzelm
parents:
52889
diff
changeset

216 
else Nil 
45459  217 
} 
218 
} 

52900
d29bf6db8a2d
more elementary list structures for markup tree traversal;
wenzelm
parents:
52889
diff
changeset

219 
traverse(root_range.start, 
d29bf6db8a2d
more elementary list structures for markup tree traversal;
wenzelm
parents:
52889
diff
changeset

220 
List((Text.Info(root_range, root_info), overlapping(root_range).toList))) 
45459  221 
} 
56301
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

222 

1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

223 
def to_XML(root_range: Text.Range, text: CharSequence, elements: Document.Elements): XML.Body = 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

224 
{ 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

225 
def make_text(start: Text.Offset, stop: Text.Offset): XML.Body = 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

226 
if (start == stop) Nil 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

227 
else List(XML.Text(text.subSequence(start, stop).toString)) 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

228 

1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

229 
def make_elems(rev_markups: List[XML.Elem], body: XML.Body): XML.Body = 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

230 
(body /: rev_markups) { 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

231 
case (b, elem) => 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

232 
if (!elements(elem.name)) b 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

233 
else if (elem.body.isEmpty) List(XML.Elem(elem.markup, b)) 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

234 
else List(XML.Wrapped_Elem(elem.markup, elem.body, b)) 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

235 
} 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

236 

1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

237 
def make_body(elem_range: Text.Range, elem_markup: List[XML.Elem], entries: Branches.T) 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

238 
: XML.Body = 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

239 
{ 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

240 
val body = new mutable.ListBuffer[XML.Tree] 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

241 
var last = elem_range.start 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

242 
for ((range, entry) < entries) { 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

243 
val subrange = range.restrict(elem_range) 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

244 
body ++= make_text(last, subrange.start) 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

245 
body ++= make_body(subrange, entry.rev_markup, entry.subtree.overlapping(subrange)) 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

246 
last = subrange.stop 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

247 
} 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

248 
body ++= make_text(last, elem_range.stop) 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

249 
make_elems(elem_markup, body.toList) 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

250 
} 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

251 
make_body(root_range, Nil, overlapping(root_range)) 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

252 
} 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

253 

1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

254 
override def toString = 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

255 
branches.toList.map(_._2) match { 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

256 
case Nil => "Empty" 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

257 
case list => list.mkString("Tree(", ",", ")") 
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56300
diff
changeset

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

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

260 