src/Pure/PIDE/markup_tree.scala
author wenzelm
Wed Aug 18 23:44:50 2010 +0200 (2010-08-18)
changeset 38479 e628da370072
parent 38478 src/Pure/PIDE/markup_node.scala@7766812a01e7
child 38482 7b6ee937b75f
permissions -rw-r--r--
more efficient Markup_Tree, based on branches sorted by quasi-order;
renamed markup_node.scala to markup_tree.scala and classes/objects accordingly;
Position.Range: produce actual Text.Range;
Symbol.Index.decode: convert 1-based Isabelle offsets here;
added static Command.range;
simplified Command.markup;
Document_Model.token_marker: flatten markup at most once;
tuned;
     1 /*  Title:      Pure/PIDE/markup_tree.scala
     2     Author:     Fabian Immler, TU Munich
     3     Author:     Makarius
     4 
     5 Markup trees over nested / non-overlapping text ranges.
     6 */
     7 
     8 package isabelle
     9 
    10 
    11 import javax.swing.tree.DefaultMutableTreeNode
    12 
    13 import scala.collection.immutable.SortedMap
    14 import scala.collection.mutable
    15 import scala.annotation.tailrec
    16 
    17 
    18 object Markup_Tree
    19 {
    20   case class Node(val range: Text.Range, val info: Any)
    21 
    22 
    23   /* branches sorted by quasi-order -- overlapping intervals appear as equivalent */
    24 
    25   object Branches
    26   {
    27     type Entry = (Node, Markup_Tree)
    28     type T = SortedMap[Node, Entry]
    29 
    30     val empty = SortedMap.empty[Node, Entry](new scala.math.Ordering[Node]
    31       {
    32         def compare(x: Node, y: Node): Int = x.range compare y.range
    33       })
    34     def update(branches: T, entries: Entry*): T =
    35       branches ++ entries.map(e => (e._1 -> e))
    36     def make(entries: List[Entry]): T = update(empty, entries:_*)
    37   }
    38 
    39   val empty = new Markup_Tree(Branches.empty)
    40 }
    41 
    42 
    43 case class Markup_Tree(val branches: Markup_Tree.Branches.T)
    44 {
    45   import Markup_Tree._
    46 
    47   def + (new_node: Node): Markup_Tree =
    48   {
    49     // FIXME tune overlapping == branches && rest.isEmpty
    50     val (overlapping, rest) =
    51     {
    52       val overlapping = new mutable.ListBuffer[Branches.Entry]
    53       var rest = branches
    54       while (rest.isDefinedAt(new_node)) {
    55         overlapping += rest(new_node)
    56         rest -= new_node
    57       }
    58       (overlapping.toList, rest)
    59     }
    60     overlapping match {
    61       case Nil =>
    62         new Markup_Tree(Branches.update(branches, new_node -> empty))
    63 
    64       case List((node, subtree))
    65         if node.range != new_node.range && (node.range contains new_node.range) =>
    66         new Markup_Tree(Branches.update(branches, node -> (subtree + new_node)))
    67 
    68       case _ if overlapping.forall(e => new_node.range contains e._1.range) =>
    69         val new_tree = new Markup_Tree(Branches.make(overlapping))
    70         new Markup_Tree(Branches.update(rest, new_node -> new_tree))
    71 
    72       case _ => // FIXME split markup!?
    73         System.err.println("Ignored overlapping markup: " + new_node); this
    74     }
    75   }
    76 
    77   // FIXME depth-first with result markup stack
    78   // FIXME projection to given range
    79   def flatten(parent: Node): List[Node] =
    80   {
    81     val result = new mutable.ListBuffer[Node]
    82     var offset = parent.range.start
    83     for ((_, (node, subtree)) <- branches.iterator) {
    84       if (offset < node.range.start)
    85         result += new Node(Text.Range(offset, node.range.start), parent.info)
    86       result ++= subtree.flatten(node)
    87       offset = node.range.stop
    88     }
    89     if (offset < parent.range.stop)
    90       result += new Node(Text.Range(offset, parent.range.stop), parent.info)
    91     result.toList
    92   }
    93 
    94   def filter(pred: Node => Boolean): Markup_Tree =
    95   {
    96     val bs = branches.toList.flatMap(entry => {
    97       val (_, (node, subtree)) = entry
    98       if (pred(node)) List((node, (node, subtree.filter(pred))))
    99       else subtree.filter(pred).branches.toList
   100     })
   101     new Markup_Tree(Branches.empty ++ bs)
   102   }
   103 
   104   def swing_tree(parent: DefaultMutableTreeNode)(swing_node: Node => DefaultMutableTreeNode)
   105   {
   106     for ((_, (node, subtree)) <- branches) {
   107       val current = swing_node(node)
   108       subtree.swing_tree(current)(swing_node)
   109       parent.add(current)
   110     }
   111   }
   112 }
   113