1/* Title: Pure/PIDE/markup_tree.scala 2 Author: Fabian Immler, TU Munich 3 Author: Makarius 4 5Markup trees over nested / non-overlapping text ranges. 6*/ 7 8package isabelle 9 10 11import scala.collection.immutable.SortedMap 12import scala.collection.mutable 13import scala.annotation.tailrec 14 15 16object Markup_Tree 17{ 18 /* construct trees */ 19 20 val empty: Markup_Tree = new Markup_Tree(Branches.empty) 21 22 def merge(trees: List[Markup_Tree], range: Text.Range, elements: Markup.Elements): Markup_Tree = 23 (empty /: trees)(_.merge(_, range, elements)) 24 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 40 41 /* tree building blocks */ 42 43 object Entry 44 { 45 def apply(markup: Text.Markup, subtree: Markup_Tree): Entry = 46 Entry(markup.range, List(markup.info), subtree) 47 } 48 49 sealed case class Entry( 50 range: Text.Range, 51 rev_markup: List[XML.Elem], 52 subtree: Markup_Tree) 53 { 54 def markup: List[XML.Elem] = rev_markup.reverse 55 56 def filter_markup(elements: Markup.Elements): List[XML.Elem] = 57 { 58 var result: List[XML.Elem] = Nil 59 for (elem <- rev_markup if elements(elem.name)) 60 result ::= elem 61 result.toList 62 } 63 64 def + (markup: Text.Markup): Entry = copy(rev_markup = markup.info :: rev_markup) 65 def \ (markup: Text.Markup): Entry = copy(subtree = subtree + markup) 66 } 67 68 object Branches 69 { 70 type T = SortedMap[Text.Range, Entry] 71 val empty: T = SortedMap.empty(Text.Range.Ordering) 72 } 73 74 75 /* XML representation */ 76 77 @tailrec private def strip_elems( 78 elems: List[XML.Elem], body: XML.Body): (List[XML.Elem], XML.Body) = 79 body match { 80 case List(XML.Wrapped_Elem(markup1, body1, body2)) => 81 strip_elems(XML.Elem(markup1, body1) :: elems, body2) 82 case List(XML.Elem(markup1, body1)) => 83 strip_elems(XML.Elem(markup1, Nil) :: elems, body1) 84 case _ => (elems, body) 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) 94 95 case (elems, body) => 96 val (end_offset, subtrees) = ((offset, Nil: List[Markup_Tree]) /: body)(make_trees) 97 if (offset == end_offset) acc 98 else { 99 val range = Text.Range(offset, end_offset) 100 val entry = Entry(range, elems, merge_disjoint(subtrees)) 101 (end_offset, new Markup_Tree(Branches.empty, entry) :: markup_trees) 102 } 103 } 104 } 105 106 def from_XML(body: XML.Body): Markup_Tree = 107 merge_disjoint(((0, Nil: List[Markup_Tree]) /: body)(make_trees)._2) 108} 109 110 111final class Markup_Tree private(val branches: Markup_Tree.Branches.T) 112{ 113 import Markup_Tree._ 114 115 private def this(branches: Markup_Tree.Branches.T, entry: Markup_Tree.Entry) = 116 this(branches + (entry.range -> entry)) 117 118 private def overlapping(range: Text.Range): Branches.T = 119 if (branches.isEmpty || 120 (range.contains(branches.firstKey.start) && branches.lastKey.stop <= range.stop)) 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 } 130 } 131 132 def restrict(range: Text.Range): Markup_Tree = 133 new Markup_Tree(overlapping(range)) 134 135 def is_empty: Boolean = branches.isEmpty 136 137 def + (new_markup: Text.Markup): Markup_Tree = 138 { 139 val new_range = new_markup.range 140 141 branches.get(new_range) match { 142 case None => new Markup_Tree(branches, Entry(new_markup, empty)) 143 case Some(entry) => 144 if (entry.range == new_range) 145 new Markup_Tree(branches, entry + new_markup) 146 else if (entry.range.contains(new_range)) 147 new Markup_Tree(branches, entry \ new_markup) 148 else if (new_range.contains(branches.head._1) && new_range.contains(branches.last._1)) 149 new Markup_Tree(Branches.empty, Entry(new_markup, this)) 150 else { 151 val body = overlapping(new_range) 152 if (body.forall(e => new_range.contains(e._1))) 153 new Markup_Tree(branches -- body.keys, Entry(new_markup, new Markup_Tree(body))) 154 else { 155 Output.warning("Ignored overlapping markup information: " + new_markup + "\n" + 156 body.filter(e => !new_range.contains(e._1)).values.mkString("\n")) 157 this 158 } 159 } 160 } 161 } 162 163 def merge(other: Markup_Tree, root_range: Text.Range, elements: Markup.Elements): Markup_Tree = 164 { 165 def merge_trees(tree1: Markup_Tree, tree2: Markup_Tree): Markup_Tree = 166 (tree1 /: tree2.branches)( 167 { case (tree, (range, entry)) => 168 if (!range.overlaps(root_range)) tree 169 else 170 (merge_trees(tree, entry.subtree) /: entry.filter_markup(elements))( 171 { case (t, elem) => t + Text.Info(range, elem) }) 172 }) 173 174 if (this eq other) this 175 else { 176 val tree1 = this.restrict(root_range) 177 val tree2 = other.restrict(root_range) 178 if (tree1.is_empty) tree2 179 else merge_trees(tree1, tree2) 180 } 181 } 182 183 def cumulate[A](root_range: Text.Range, root_info: A, elements: Markup.Elements, 184 result: (A, Text.Markup) => Option[A]): List[Text.Info[A]] = 185 { 186 def results(x: A, entry: Entry): Option[A] = 187 { 188 var y = x 189 var changed = false 190 for { 191 elem <- entry.filter_markup(elements) 192 y1 <- result(y, Text.Info(entry.range, elem)) 193 } { y = y1; changed = true } 194 if (changed) Some(y) else None 195 } 196 197 def traverse( 198 last: Text.Offset, 199 stack: List[(Text.Info[A], List[(Text.Range, Entry)])]): List[Text.Info[A]] = 200 { 201 stack match { 202 case (parent, (range, entry) :: more) :: rest => 203 val subrange = range.restrict(root_range) 204 val subtree = entry.subtree.overlapping(subrange).toList 205 val start = subrange.start 206 207 results(parent.info, entry) match { 208 case Some(res) => 209 val next = Text.Info(subrange, res) 210 val nexts = traverse(start, (next, subtree) :: (parent, more) :: rest) 211 if (last < start) parent.restrict(Text.Range(last, start)) :: nexts 212 else nexts 213 case None => traverse(last, (parent, subtree ::: more) :: rest) 214 } 215 216 case (parent, Nil) :: rest => 217 val stop = parent.range.stop 218 val nexts = traverse(stop, rest) 219 if (last < stop) parent.restrict(Text.Range(last, stop)) :: nexts 220 else nexts 221 222 case Nil => 223 val stop = root_range.stop 224 if (last < stop) List(Text.Info(Text.Range(last, stop), root_info)) 225 else Nil 226 } 227 } 228 traverse(root_range.start, 229 List((Text.Info(root_range, root_info), overlapping(root_range).toList))) 230 } 231 232 def to_XML(root_range: Text.Range, text: CharSequence, elements: Markup.Elements): XML.Body = 233 { 234 def make_text(start: Text.Offset, stop: Text.Offset): XML.Body = 235 if (start == stop) Nil 236 else List(XML.Text(text.subSequence(start, stop).toString)) 237 238 def make_elems(rev_markups: List[XML.Elem], body: XML.Body): XML.Body = 239 (body /: rev_markups) { 240 case (b, elem) => 241 if (!elements(elem.name)) b 242 else if (elem.body.isEmpty) List(XML.Elem(elem.markup, b)) 243 else List(XML.Wrapped_Elem(elem.markup, elem.body, b)) 244 } 245 246 def make_body(elem_range: Text.Range, elem_markup: List[XML.Elem], entries: Branches.T) 247 : XML.Body = 248 { 249 val body = new mutable.ListBuffer[XML.Tree] 250 var last = elem_range.start 251 for ((range, entry) <- entries) { 252 val subrange = range.restrict(elem_range) 253 body ++= make_text(last, subrange.start) 254 body ++= make_body(subrange, entry.rev_markup, entry.subtree.overlapping(subrange)) 255 last = subrange.stop 256 } 257 body ++= make_text(last, elem_range.stop) 258 make_elems(elem_markup, body.toList) 259 } 260 make_body(root_range, Nil, overlapping(root_range)) 261 } 262 263 override def toString: String = 264 branches.toList.map(_._2) match { 265 case Nil => "Empty" 266 case list => list.mkString("Tree(", ",", ")") 267 } 268} 269