isabelle: src/Pure/PIDE/markup_tree.scala@33ad12ef79ff

     1 /*  Title:      Pure/PIDE/markup_tree.scala

     2     Module:     PIDE

     3     Author:     Fabian Immler, TU Munich

     4     Author:     Makarius

     6 Markup trees over nested / non-overlapping text ranges.

     7 */

     9 package isabelle

    12 import scala.collection.immutable.SortedMap

    13 import scala.collection.mutable

    14 import scala.annotation.tailrec

    17 object Markup_Tree

    18 {

    19   /* construct trees */

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

    23   def merge_disjoint(trees: List[Markup_Tree]): Markup_Tree =

    24     trees match {

    25       case Nil => empty

    26       case head :: tail =>

    27         new Markup_Tree(

    28           (head.branches /: tail) {

    29             case (branches, tree) =>

    30               (branches /: tree.branches) {

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

    32                   require(!bs.isDefinedAt(r))

    33                   bs + (r -> entry)

    34               }

    35           })

    36     }

    39   /* tree building blocks */

    41   object Entry

    42   {

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

    44       Entry(markup.range, List(markup.info), subtree)

    45   }

    47   sealed case class Entry(

    48     range: Text.Range,

    49     rev_markup: List[XML.Elem],

    50     subtree: Markup_Tree)

    51   {

    52     def markup: List[XML.Elem] = rev_markup.reverse

    54     def filter_markup(pred: String => Boolean): List[XML.Elem] =

    55     {

    56       var result: List[XML.Elem] = Nil

    57       for { elem <- rev_markup; if (pred(elem.name)) }

    58         result ::= elem

    59       result.toList

    60     }

    62     def + (markup: Text.Markup): Entry = copy(rev_markup = markup.info :: rev_markup)

    63     def \ (markup: Text.Markup): Entry = copy(subtree = subtree + markup)

    64   }

    66   object Branches

    67   {

    68     type T = SortedMap[Text.Range, Entry]

    69     val empty: T = SortedMap.empty(Text.Range.Ordering)

    70   }

    73   /* XML representation */

    75   @tailrec private def strip_elems(

    76       elems: List[XML.Elem], body: XML.Body): (List[XML.Elem], XML.Body) =

    77     body match {

    78       case List(XML.Wrapped_Elem(markup1, body1, body2)) =>

    79         strip_elems(XML.Elem(markup1, body1) :: elems, body2)

    80       case List(XML.Elem(markup1, body1)) =>

    81         strip_elems(XML.Elem(markup1, Nil) :: elems, body1)

    82       case _ => (elems, body)

    83     }

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

    86     {

    87       val (offset, markup_trees) = acc

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

    90         case (Nil, body) =>

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

    93         case (elems, body) =>

    94           val (end_offset, subtrees) = ((offset, Nil: List[Markup_Tree]) /: body)(make_trees)

    95           if (offset == end_offset) acc

    96           else {

    97             val range = Text.Range(offset, end_offset)

    98             val entry = Entry(range, elems, merge_disjoint(subtrees))

    99             (end_offset, new Markup_Tree(Branches.empty, entry) :: markup_trees)

   100           }

   101       }

   102     }

   104   def from_XML(body: XML.Body): Markup_Tree =

   105     merge_disjoint(((0, Nil: List[Markup_Tree]) /: body)(make_trees)._2)

   106 }

   109 final class Markup_Tree private(val branches: Markup_Tree.Branches.T)

   110 {

   111   import Markup_Tree._

   113   private def this(branches: Markup_Tree.Branches.T, entry: Markup_Tree.Entry) =

   114     this(branches + (entry.range -> entry))

   116   override def toString =

   117     branches.toList.map(_._2) match {

   118       case Nil => "Empty"

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

   120     }

   122   private def overlapping(range: Text.Range): Branches.T =

   123   {

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

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

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

   127     branches.get(stop) match {

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

   129       case _ => bs

   130     }

   131   }

   133   def + (new_markup: Text.Markup): Markup_Tree =

   134   {

   135     val new_range = new_markup.range

   137     branches.get(new_range) match {

   138       case None => new Markup_Tree(branches, Entry(new_markup, empty))

   139       case Some(entry) =>

   140         if (entry.range == new_range)

   141           new Markup_Tree(branches, entry + new_markup)

   142         else if (entry.range.contains(new_range))

   143           new Markup_Tree(branches, entry \ new_markup)

   144         else if (new_range.contains(branches.head._1) && new_range.contains(branches.last._1))

   145           new Markup_Tree(Branches.empty, Entry(new_markup, this))

   146         else {

   147           val body = overlapping(new_range)

   148           if (body.forall(e => new_range.contains(e._1)))

   149             new Markup_Tree(branches -- body.keys, Entry(new_markup, new Markup_Tree(body)))

   150           else {

   151             System.err.println("Ignored overlapping markup information: " + new_markup +

   152               body.filter(e => !new_range.contains(e._1)).mkString("\n"))

   153             this

   154           }

   155         }

   156     }

   157   }

   159   def ++ (other: Markup_Tree): Markup_Tree =

   160     (this /: other.branches)({ case (tree, (range, entry)) =>

   161       ((tree ++ entry.subtree) /: entry.markup)({ case (t, elem) => t + Text.Info(range, elem) }) })

   163   def to_XML(root_range: Text.Range, text: CharSequence, filter: XML.Elem => Boolean): XML.Body =

   164   {

   165     def make_text(start: Text.Offset, stop: Text.Offset): XML.Body =

   166       if (start == stop) Nil

   167       else List(XML.Text(text.subSequence(start, stop).toString))

   169     def make_elems(rev_markups: List[XML.Elem], body: XML.Body): XML.Body =

   170       (body /: rev_markups) {

   171         case (b, elem) =>

   172           if (!filter(elem)) b

   173           else if (elem.body.isEmpty) List(XML.Elem(elem.markup, b))

   174           else List(XML.Wrapped_Elem(elem.markup, elem.body, b))

   175       }

   177     def make_body(elem_range: Text.Range, elem_markup: List[XML.Elem], entries: Branches.T)

   178       : XML.Body =

   179     {

   180       val body = new mutable.ListBuffer[XML.Tree]

   181       var last = elem_range.start

   182       for ((range, entry) <- entries) {

   183         val subrange = range.restrict(elem_range)

   184         body ++= make_text(last, subrange.start)

   185         body ++= make_body(subrange, entry.rev_markup, entry.subtree.overlapping(subrange))

   186         last = subrange.stop

   187       }

   188       body ++= make_text(last, elem_range.stop)

   189       make_elems(elem_markup, body.toList)

   190     }

   191    make_body(root_range, Nil, overlapping(root_range))

   192   }

   194   def to_XML(text: CharSequence): XML.Body =

   195     to_XML(Text.Range(0, text.length), text, (_: XML.Elem) => true)

   197   def cumulate[A](root_range: Text.Range, root_info: A, elements: String => Boolean,

   198     result: (A, Text.Markup) => Option[A]): List[Text.Info[A]] =

   199   {

   200     def results(x: A, entry: Entry): Option[A] =

   201     {

   202       var y = x

   203       var changed = false

   204       for {

   205         elem <- entry.filter_markup(elements)

   206         y1 <- result(y, Text.Info(entry.range, elem))

   207       } { y = y1; changed = true }

   208       if (changed) Some(y) else None

   209     }

   211     def traverse(

   212       last: Text.Offset,

   213       stack: List[(Text.Info[A], List[(Text.Range, Entry)])]): List[Text.Info[A]] =

   214     {

   215       stack match {

   216         case (parent, (range, entry) :: more) :: rest =>

   217           val subrange = range.restrict(root_range)

   218           val subtree = entry.subtree.overlapping(subrange).toList

   219           val start = subrange.start

   221           results(parent.info, entry) match {

   222             case Some(res) =>

   223               val next = Text.Info(subrange, res)

   224               val nexts = traverse(start, (next, subtree) :: (parent, more) :: rest)

   225               if (last < start) parent.restrict(Text.Range(last, start)) :: nexts

   226               else nexts

   227             case None => traverse(last, (parent, subtree ::: more) :: rest)

   228           }

   230         case (parent, Nil) :: rest =>

   231           val stop = parent.range.stop

   232           val nexts = traverse(stop, rest)

   233           if (last < stop) parent.restrict(Text.Range(last, stop)) :: nexts

   234           else nexts

   236         case Nil =>

   237           val stop = root_range.stop

   238           if (last < stop) List(Text.Info(Text.Range(last, stop), root_info))

   239           else Nil

   240       }

   241     }

   242     traverse(root_range.start,

   243       List((Text.Info(root_range, root_info), overlapping(root_range).toList)))

   244   }

   245 }

author	wenzelm
	Fri Feb 21 16:14:35 2014 +0100 (2014-02-21)
changeset 55652	33ad12ef79ff
parent 55645	561754277494
child 55820	61869776ce1f
permissions	-rw-r--r--