src/Pure/PIDE/markup_tree.scala
author wenzelm
Thu Sep 20 13:34:27 2012 +0200 (2012-09-20)
changeset 49467 25b7e843e124
parent 49466 99ed1f422635
child 49469 00c301c8d569
permissions -rw-r--r--
more direct Markup_Tree.from_XML;
     1 /*  Title:      Pure/PIDE/markup_tree.scala
     2     Module:     PIDE
     3     Author:     Fabian Immler, TU Munich
     4     Author:     Makarius
     5 
     6 Markup trees over nested / non-overlapping text ranges.
     7 */
     8 
     9 package isabelle
    10 
    11 import java.lang.System
    12 import javax.swing.tree.DefaultMutableTreeNode
    13 
    14 import scala.collection.immutable.SortedMap
    15 import scala.annotation.tailrec
    16 
    17 
    18 object Markup_Tree
    19 {
    20   val empty: Markup_Tree = new Markup_Tree(Branches.empty)
    21 
    22   def merge_disjoint(trees: List[Markup_Tree]): Markup_Tree =
    23     trees match {
    24       case Nil => empty
    25       case head :: tail =>
    26         new Markup_Tree(
    27           (head.branches /: tail) {
    28             case (branches, tree) =>
    29               (branches /: tree.branches) {
    30                 case (bs, (r, entry)) =>
    31                   require(!bs.isDefinedAt(r))
    32                   bs + (r -> entry)
    33               }
    34           })
    35     }
    36 
    37   object Entry
    38   {
    39     def apply(markup: Text.Markup, subtree: Markup_Tree): Entry =
    40       Entry(markup.range, List(markup.info), Set(markup.info.markup.name), subtree)
    41   }
    42 
    43   sealed case class Entry(
    44     range: Text.Range,
    45     rev_markup: List[XML.Elem],
    46     elements: Set[String],
    47     subtree: Markup_Tree)
    48   {
    49     def + (info: XML.Elem): Entry =
    50       if (elements(info.markup.name)) copy(rev_markup = info :: rev_markup)
    51       else copy(rev_markup = info :: rev_markup, elements = elements + info.markup.name)
    52 
    53     def markup: List[XML.Elem] = rev_markup.reverse
    54   }
    55 
    56   object Branches
    57   {
    58     type T = SortedMap[Text.Range, Entry]
    59     val empty: T = SortedMap.empty(Text.Range.Ordering)
    60   }
    61 
    62 
    63   /* XML representation */
    64 
    65   @tailrec private def strip_elems(markups: List[Markup], body: XML.Body): (List[Markup], XML.Body) =
    66     body match {
    67       case List(XML.Elem(markup1, body1)) => strip_elems(markup1 :: markups, body1)
    68       case _ => (markups, body)
    69     }
    70 
    71   private def make_trees(acc: (Int, List[Markup_Tree]), tree: XML.Tree): (Int, List[Markup_Tree]) =
    72     {
    73       val (offset, markup_trees) = acc
    74 
    75       strip_elems(Nil, List(tree)) match {
    76         case (Nil, body) =>
    77           (offset + XML.text_length(body), markup_trees)
    78 
    79         case (markups, body) =>
    80           val (end_offset, markup_trees1) = (acc /: body)(make_trees)
    81           val range = Text.Range(offset, end_offset)
    82           val new_markup_tree =
    83             (merge_disjoint(markup_trees1) /: markups) {
    84               case (markup_tree, markup) =>
    85                 markup_tree + Text.Info(range, XML.Elem(markup, Nil))
    86             }
    87           (end_offset, List(new_markup_tree))
    88       }
    89     }
    90 
    91   def from_XML(body: XML.Body): Markup_Tree =
    92     merge_disjoint(((0, Nil: List[Markup_Tree]) /: body)(make_trees)._2)
    93 }
    94 
    95 
    96 final class Markup_Tree private(private val branches: Markup_Tree.Branches.T)
    97 {
    98   import Markup_Tree._
    99 
   100   private def this(branches: Markup_Tree.Branches.T, entry: Markup_Tree.Entry) =
   101     this(branches + (entry.range -> entry))
   102 
   103   override def toString =
   104     branches.toList.map(_._2) match {
   105       case Nil => "Empty"
   106       case list => list.mkString("Tree(", ",", ")")
   107     }
   108 
   109   private def overlapping(range: Text.Range): Branches.T =
   110   {
   111     val start = Text.Range(range.start)
   112     val stop = Text.Range(range.stop)
   113     val bs = branches.range(start, stop)
   114     // FIXME check after Scala 2.8.x
   115     branches.get(stop) match {
   116       case Some(end) if range overlaps end.range => bs + (end.range -> end)
   117       case _ => bs
   118     }
   119   }
   120 
   121   def + (new_markup: Text.Markup): Markup_Tree =
   122   {
   123     val new_range = new_markup.range
   124 
   125     branches.get(new_range) match {
   126       case None => new Markup_Tree(branches, Entry(new_markup, empty))
   127       case Some(entry) =>
   128         if (entry.range == new_range)
   129           new Markup_Tree(branches, entry + new_markup.info)
   130         else if (entry.range.contains(new_range))
   131           new Markup_Tree(branches, entry.copy(subtree = entry.subtree + new_markup))
   132         else if (new_range.contains(branches.head._1) && new_range.contains(branches.last._1))
   133           new Markup_Tree(Branches.empty, Entry(new_markup, this))
   134         else {
   135           val body = overlapping(new_range)
   136           if (body.forall(e => new_range.contains(e._1))) {
   137             val rest = // branches -- body, modulo workarounds for Redblack in Scala 2.8.0 FIXME
   138               if (body.size > 1)
   139                 (Branches.empty /: branches)((rest, entry) =>
   140                   if (body.isDefinedAt(entry._1)) rest else rest + entry)
   141               else branches
   142             new Markup_Tree(rest, Entry(new_markup, new Markup_Tree(body)))
   143           }
   144           else { // FIXME split markup!?
   145             System.err.println("Ignored overlapping markup information: " + new_markup +
   146               body.filter(e => !new_range.contains(e._1)).mkString("\n"))
   147             this
   148           }
   149         }
   150     }
   151   }
   152 
   153   def cumulate[A](root_range: Text.Range, root_info: A, result_elements: Option[Set[String]],
   154     result: PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]] =
   155   {
   156     def results(x: A, entry: Entry): Option[A] =
   157       if (result_elements match { case Some(es) => es.exists(entry.elements) case None => true }) {
   158         val (y, changed) =
   159           (entry.markup :\ (x, false))((info, res) =>
   160             {
   161               val (y, changed) = res
   162               val arg = (y, Text.Info(entry.range, info))
   163               if (result.isDefinedAt(arg)) (result(arg), true)
   164               else res
   165             })
   166         if (changed) Some(y) else None
   167       }
   168       else None
   169 
   170     def stream(
   171       last: Text.Offset,
   172       stack: List[(Text.Info[A], Stream[(Text.Range, Entry)])]): Stream[Text.Info[A]] =
   173     {
   174       stack match {
   175         case (parent, (range, entry) #:: more) :: rest =>
   176           val subrange = range.restrict(root_range)
   177           val subtree = entry.subtree.overlapping(subrange).toStream
   178           val start = subrange.start
   179 
   180           results(parent.info, entry) match {
   181             case Some(res) =>
   182               val next = Text.Info(subrange, res)
   183               val nexts = stream(start, (next, subtree) :: (parent, more) :: rest)
   184               if (last < start) parent.restrict(Text.Range(last, start)) #:: nexts
   185               else nexts
   186             case None => stream(last, (parent, subtree #::: more) :: rest)
   187           }
   188 
   189         case (parent, Stream.Empty) :: rest =>
   190           val stop = parent.range.stop
   191           val nexts = stream(stop, rest)
   192           if (last < stop) parent.restrict(Text.Range(last, stop)) #:: nexts
   193           else nexts
   194 
   195         case Nil =>
   196           val stop = root_range.stop
   197           if (last < stop) Stream(Text.Info(Text.Range(last, stop), root_info))
   198           else Stream.empty
   199       }
   200     }
   201     stream(root_range.start,
   202       List((Text.Info(root_range, root_info), overlapping(root_range).toStream)))
   203   }
   204 
   205   def swing_tree(parent: DefaultMutableTreeNode,
   206     swing_node: Text.Info[List[XML.Elem]] => DefaultMutableTreeNode)
   207   {
   208     for ((_, entry) <- branches) {
   209       val node = swing_node(Text.Info(entry.range, entry.markup))
   210       entry.subtree.swing_tree(node, swing_node)
   211       parent.add(node)
   212     }
   213   }
   214 }
   215