author  wenzelm 
Sat, 05 Dec 2020 11:49:04 +0100  
changeset 72815  85aaaf2cd173 
parent 71383  8313dca6dee9 
child 73120  c3589f2dff31 
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 

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

11 
import scala.collection.immutable.SortedMap 
49614  12 
import scala.collection.mutable 
49467  13 
import scala.annotation.tailrec 
38479
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 
{ 
50551  18 
/* construct trees */ 
19 

45456  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 

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

23 
(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

24 

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

27 
case Nil => empty 

28 
case head :: tail => 

29 
new Markup_Tree( 

30 
(head.branches /: tail) { 

31 
case (branches, tree) => 

32 
(branches /: tree.branches) { 

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

34 
require(!bs.isDefinedAt(r)) 

35 
bs + (r > entry) 

36 
} 

37 
}) 

38 
} 

39 

50551  40 

41 
/* tree building blocks */ 

42 

45473  43 
object Entry 
44 
{ 

45 
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

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

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

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

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

51 
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

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

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

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

55 

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

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

58 
var result: List[XML.Elem] = Nil 
60215  59 
for (elem < rev_markup if elements(elem.name)) 
55645
561754277494
tuned  remaining rev_markup is rather short after filter;
wenzelm
parents:
55622
diff
changeset

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

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

63 

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

64 
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

65 
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

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

67 

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

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

69 
{ 
38578  70 
type T = SortedMap[Text.Range, Entry] 
45456  71 
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

72 
} 
49466  73 

74 

75 
/* XML representation */ 

76 

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

77 
@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

78 
elems: List[XML.Elem], body: XML.Body): (List[XML.Elem], XML.Body) = 
49467  79 
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

80 
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

81 
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

82 
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

83 
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

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

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

88 
{ 

89 
val (offset, markup_trees) = acc 

90 

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

92 
case (Nil, body) => 

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

49466  94 

49469  95 
case (elems, body) => 
96 
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

97 
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

98 
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

99 
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

100 
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

101 
(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

102 
} 
49466  103 
} 
49467  104 
} 
49466  105 

49467  106 
def from_XML(body: XML.Body): Markup_Tree = 
107 
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

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

109 

34393  110 

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

111 
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

112 
{ 
49417  113 
import Markup_Tree._ 
114 

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

115 
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

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

117 

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

118 
private def overlapping(range: Text.Range): Branches.T = 
56311  119 
if (branches.isEmpty  
56313  120 
(range.contains(branches.firstKey.start) && branches.lastKey.stop <= range.stop)) 
56311  121 
branches 
122 
else { 

123 
val start = Text.Range(range.start) 

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

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

126 
branches.get(stop) match { 

127 
case Some(end) if range overlaps end.range => bs + (end.range > end) 

128 
case _ => bs 

129 
} 

45457  130 
} 
131 

56307
2bdf8261677a
more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
wenzelm
parents:
56302
diff
changeset

132 
def restrict(range: Text.Range): Markup_Tree = 
2bdf8261677a
more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
wenzelm
parents:
56302
diff
changeset

133 
new Markup_Tree(overlapping(range)) 
2bdf8261677a
more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
wenzelm
parents:
56302
diff
changeset

134 

2bdf8261677a
more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
wenzelm
parents:
56302
diff
changeset

135 
def is_empty: Boolean = branches.isEmpty 
2bdf8261677a
more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
wenzelm
parents:
56302
diff
changeset

136 

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

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

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

140 

38578  141 
branches.get(new_range) match { 
45473  142 
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

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

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

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

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

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

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

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

153 
new Markup_Tree(branches  body.keys, Entry(new_markup, new Markup_Tree(body))) 
49608  154 
else { 
58463  155 
Output.warning("Ignored overlapping markup information: " + new_markup + "\n" + 
71383  156 
body.filter(e => !new_range.contains(e._1)).values.mkString("\n")) 
38482
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset

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

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

159 
} 
34703  160 
} 
161 
} 

162 

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

165 
def merge_trees(tree1: Markup_Tree, tree2: Markup_Tree): Markup_Tree = 
56307
2bdf8261677a
more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
wenzelm
parents:
56302
diff
changeset

166 
(tree1 /: tree2.branches)( 
2bdf8261677a
more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
wenzelm
parents:
56302
diff
changeset

167 
{ case (tree, (range, entry)) => 
2bdf8261677a
more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
wenzelm
parents:
56302
diff
changeset

168 
if (!range.overlaps(root_range)) tree 
2bdf8261677a
more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
wenzelm
parents:
56302
diff
changeset

169 
else 
2bdf8261677a
more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
wenzelm
parents:
56302
diff
changeset

170 
(merge_trees(tree, entry.subtree) /: entry.filter_markup(elements))( 
2bdf8261677a
more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
wenzelm
parents:
56302
diff
changeset

171 
{ case (t, elem) => t + Text.Info(range, elem) }) 
2bdf8261677a
more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
wenzelm
parents:
56302
diff
changeset

172 
}) 
49614  173 

56307
2bdf8261677a
more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
wenzelm
parents:
56302
diff
changeset

174 
if (this eq other) this 
2bdf8261677a
more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
wenzelm
parents:
56302
diff
changeset

175 
else { 
2bdf8261677a
more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
wenzelm
parents:
56302
diff
changeset

176 
val tree1 = this.restrict(root_range) 
2bdf8261677a
more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
wenzelm
parents:
56302
diff
changeset

177 
val tree2 = other.restrict(root_range) 
2bdf8261677a
more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
wenzelm
parents:
56302
diff
changeset

178 
if (tree1.is_empty) tree2 
2bdf8261677a
more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
wenzelm
parents:
56302
diff
changeset

179 
else merge_trees(tree1, tree2) 
2bdf8261677a
more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
wenzelm
parents:
56302
diff
changeset

180 
} 
49614  181 
} 
182 

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

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

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

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

188 
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

189 
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

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

191 
elem < entry.filter_markup(elements) 
55620  192 
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

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

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

195 
} 
45467  196 

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

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

199 
stack: List[(Text.Info[A], List[(Text.Range, Entry)])]): List[Text.Info[A]] = 
45459  200 
{ 
201 
stack match { 

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

202 
case (parent, (range, entry) :: more) :: rest => 
45467  203 
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

204 
val subtree = entry.subtree.overlapping(subrange).toList 
45459  205 
val start = subrange.start 
206 

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

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

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

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

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

211 
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

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

213 
case None => traverse(last, (parent, subtree ::: more) :: rest) 
45459  214 
} 
215 

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

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

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

219 
if (last < stop) parent.restrict(Text.Range(last, stop)) :: nexts 
45459  220 
else nexts 
221 

222 
case Nil => 

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

224 
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

225 
else Nil 
45459  226 
} 
227 
} 

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

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

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

231 

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

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

234 
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

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

236 
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

237 

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

238 
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

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

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

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

242 
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

243 
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

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

245 

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

246 
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

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

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

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

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

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

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

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

254 
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

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

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

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

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

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

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

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

262 

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

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

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

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

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

268 
} 