src/Pure/PIDE/markup_tree.scala
changeset 38479 e628da370072
parent 38478 7766812a01e7
child 38482 7b6ee937b75f
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Wed Aug 18 23:44:50 2010 +0200
     1.3 @@ -0,0 +1,113 @@
     1.4 +/*  Title:      Pure/PIDE/markup_tree.scala
     1.5 +    Author:     Fabian Immler, TU Munich
     1.6 +    Author:     Makarius
     1.7 +
     1.8 +Markup trees over nested / non-overlapping text ranges.
     1.9 +*/
    1.10 +
    1.11 +package isabelle
    1.12 +
    1.13 +
    1.14 +import javax.swing.tree.DefaultMutableTreeNode
    1.15 +
    1.16 +import scala.collection.immutable.SortedMap
    1.17 +import scala.collection.mutable
    1.18 +import scala.annotation.tailrec
    1.19 +
    1.20 +
    1.21 +object Markup_Tree
    1.22 +{
    1.23 +  case class Node(val range: Text.Range, val info: Any)
    1.24 +
    1.25 +
    1.26 +  /* branches sorted by quasi-order -- overlapping intervals appear as equivalent */
    1.27 +
    1.28 +  object Branches
    1.29 +  {
    1.30 +    type Entry = (Node, Markup_Tree)
    1.31 +    type T = SortedMap[Node, Entry]
    1.32 +
    1.33 +    val empty = SortedMap.empty[Node, Entry](new scala.math.Ordering[Node]
    1.34 +      {
    1.35 +        def compare(x: Node, y: Node): Int = x.range compare y.range
    1.36 +      })
    1.37 +    def update(branches: T, entries: Entry*): T =
    1.38 +      branches ++ entries.map(e => (e._1 -> e))
    1.39 +    def make(entries: List[Entry]): T = update(empty, entries:_*)
    1.40 +  }
    1.41 +
    1.42 +  val empty = new Markup_Tree(Branches.empty)
    1.43 +}
    1.44 +
    1.45 +
    1.46 +case class Markup_Tree(val branches: Markup_Tree.Branches.T)
    1.47 +{
    1.48 +  import Markup_Tree._
    1.49 +
    1.50 +  def + (new_node: Node): Markup_Tree =
    1.51 +  {
    1.52 +    // FIXME tune overlapping == branches && rest.isEmpty
    1.53 +    val (overlapping, rest) =
    1.54 +    {
    1.55 +      val overlapping = new mutable.ListBuffer[Branches.Entry]
    1.56 +      var rest = branches
    1.57 +      while (rest.isDefinedAt(new_node)) {
    1.58 +        overlapping += rest(new_node)
    1.59 +        rest -= new_node
    1.60 +      }
    1.61 +      (overlapping.toList, rest)
    1.62 +    }
    1.63 +    overlapping match {
    1.64 +      case Nil =>
    1.65 +        new Markup_Tree(Branches.update(branches, new_node -> empty))
    1.66 +
    1.67 +      case List((node, subtree))
    1.68 +        if node.range != new_node.range && (node.range contains new_node.range) =>
    1.69 +        new Markup_Tree(Branches.update(branches, node -> (subtree + new_node)))
    1.70 +
    1.71 +      case _ if overlapping.forall(e => new_node.range contains e._1.range) =>
    1.72 +        val new_tree = new Markup_Tree(Branches.make(overlapping))
    1.73 +        new Markup_Tree(Branches.update(rest, new_node -> new_tree))
    1.74 +
    1.75 +      case _ => // FIXME split markup!?
    1.76 +        System.err.println("Ignored overlapping markup: " + new_node); this
    1.77 +    }
    1.78 +  }
    1.79 +
    1.80 +  // FIXME depth-first with result markup stack
    1.81 +  // FIXME projection to given range
    1.82 +  def flatten(parent: Node): List[Node] =
    1.83 +  {
    1.84 +    val result = new mutable.ListBuffer[Node]
    1.85 +    var offset = parent.range.start
    1.86 +    for ((_, (node, subtree)) <- branches.iterator) {
    1.87 +      if (offset < node.range.start)
    1.88 +        result += new Node(Text.Range(offset, node.range.start), parent.info)
    1.89 +      result ++= subtree.flatten(node)
    1.90 +      offset = node.range.stop
    1.91 +    }
    1.92 +    if (offset < parent.range.stop)
    1.93 +      result += new Node(Text.Range(offset, parent.range.stop), parent.info)
    1.94 +    result.toList
    1.95 +  }
    1.96 +
    1.97 +  def filter(pred: Node => Boolean): Markup_Tree =
    1.98 +  {
    1.99 +    val bs = branches.toList.flatMap(entry => {
   1.100 +      val (_, (node, subtree)) = entry
   1.101 +      if (pred(node)) List((node, (node, subtree.filter(pred))))
   1.102 +      else subtree.filter(pred).branches.toList
   1.103 +    })
   1.104 +    new Markup_Tree(Branches.empty ++ bs)
   1.105 +  }
   1.106 +
   1.107 +  def swing_tree(parent: DefaultMutableTreeNode)(swing_node: Node => DefaultMutableTreeNode)
   1.108 +  {
   1.109 +    for ((_, (node, subtree)) <- branches) {
   1.110 +      val current = swing_node(node)
   1.111 +      subtree.swing_tree(current)(swing_node)
   1.112 +      parent.add(current)
   1.113 +    }
   1.114 +  }
   1.115 +}
   1.116 +