src/Pure/PIDE/markup_tree.scala
changeset 38564 a6e2715fac5f
parent 38563 f6c9a4f9f66f
child 38566 8176107637ce
     1.1 --- a/src/Pure/PIDE/markup_tree.scala	Thu Aug 19 22:26:15 2010 +0200
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Thu Aug 19 22:52:00 2010 +0200
     1.3 @@ -17,10 +17,10 @@
     1.4  
     1.5  object Markup_Tree
     1.6  {
     1.7 -  case class Node(val range: Text.Range, val info: Any)
     1.8 +  case class Node[A](val range: Text.Range, val info: A)
     1.9    {
    1.10 -    def contains(that: Node): Boolean = this.range contains that.range
    1.11 -    def restrict(r: Text.Range): Node = Node(range.intersect(r), info)
    1.12 +    def contains[B](that: Node[B]): Boolean = this.range contains that.range
    1.13 +    def restrict(r: Text.Range): Node[A] = Node(range.restrict(r), info)
    1.14    }
    1.15  
    1.16  
    1.17 @@ -28,12 +28,12 @@
    1.18  
    1.19    object Branches
    1.20    {
    1.21 -    type Entry = (Node, Markup_Tree)
    1.22 -    type T = SortedMap[Node, Entry]
    1.23 +    type Entry = (Node[Any], Markup_Tree)
    1.24 +    type T = SortedMap[Node[Any], Entry]
    1.25  
    1.26 -    val empty = SortedMap.empty[Node, Entry](new scala.math.Ordering[Node]
    1.27 +    val empty = SortedMap.empty[Node[Any], Entry](new scala.math.Ordering[Node[Any]]
    1.28        {
    1.29 -        def compare(x: Node, y: Node): Int = x.range compare y.range
    1.30 +        def compare(x: Node[Any], y: Node[Any]): Int = x.range compare y.range
    1.31        })
    1.32  
    1.33      def update(branches: T, entry: Entry): T = branches + (entry._1 -> entry)
    1.34 @@ -56,7 +56,7 @@
    1.35        case list => list.mkString("Tree(", ",", ")")
    1.36      }
    1.37  
    1.38 -  def + (new_node: Node): Markup_Tree =
    1.39 +  def + (new_node: Node[Any]): Markup_Tree =
    1.40    {
    1.41      branches.get(new_node) match {
    1.42        case None =>
    1.43 @@ -82,9 +82,9 @@
    1.44  
    1.45    // FIXME depth-first with result markup stack
    1.46    // FIXME projection to given range
    1.47 -  def flatten(parent: Node): List[Node] =
    1.48 +  def flatten(parent: Node[Any]): List[Node[Any]] =
    1.49    {
    1.50 -    val result = new mutable.ListBuffer[Node]
    1.51 +    val result = new mutable.ListBuffer[Node[Any]]
    1.52      var offset = parent.range.start
    1.53      for ((_, (node, subtree)) <- branches.iterator) {
    1.54        if (offset < node.range.start)
    1.55 @@ -97,7 +97,7 @@
    1.56      result.toList
    1.57    }
    1.58  
    1.59 -  def filter(pred: Node => Boolean): Markup_Tree =
    1.60 +  def filter(pred: Node[Any] => Boolean): Markup_Tree =
    1.61    {
    1.62      val bs = branches.toList.flatMap(entry => {
    1.63        val (_, (node, subtree)) = entry
    1.64 @@ -107,24 +107,26 @@
    1.65      new Markup_Tree(Branches.empty ++ bs)
    1.66    }
    1.67  
    1.68 -  def select[A](range: Text.Range)(sel: PartialFunction[Node, A]): Stream[Node] =
    1.69 +  def select[A](range: Text.Range)(sel: PartialFunction[Any, A]): Stream[Node[List[A]]] =
    1.70    {
    1.71 -    def stream(parent: Node, bs: Branches.T): Stream[Node] =
    1.72 +    def stream(parent: Node[List[A]], bs: Branches.T): Stream[Node[List[A]]] =
    1.73      {
    1.74        val substream =
    1.75          (for ((_, (node, subtree)) <- Branches.overlapping(parent.range, bs).toStream) yield {
    1.76 -          if (sel.isDefinedAt(node))
    1.77 -            stream(node.restrict(parent.range), subtree.branches)
    1.78 +          if (sel.isDefinedAt(node.info)) {
    1.79 +            val current = Node(node.range.restrict(parent.range), List(sel(node.info)))
    1.80 +            stream(current, subtree.branches)
    1.81 +          }
    1.82            else stream(parent, subtree.branches)
    1.83          }).flatten
    1.84  
    1.85 -      def padding(last: Text.Offset, s: Stream[Node]): Stream[Node] =
    1.86 +      def padding(last: Text.Offset, s: Stream[Node[List[A]]]): Stream[Node[List[A]]] =
    1.87          s match {
    1.88            case (node @ Node(Text.Range(start, stop), _)) #:: rest =>
    1.89              if (last < start)
    1.90                parent.restrict(Text.Range(last, start)) #:: node #:: padding(stop, rest)
    1.91              else node #:: padding(stop, rest)
    1.92 -          case Stream.Empty =>  // FIXME
    1.93 +          case Stream.Empty =>
    1.94              if (last < parent.range.stop)
    1.95                Stream(parent.restrict(Text.Range(last, parent.range.stop)))
    1.96              else Stream.Empty
    1.97 @@ -134,7 +136,7 @@
    1.98      stream(Node(range, Nil), branches)
    1.99    }
   1.100  
   1.101 -  def swing_tree(parent: DefaultMutableTreeNode)(swing_node: Node => DefaultMutableTreeNode)
   1.102 +  def swing_tree(parent: DefaultMutableTreeNode)(swing_node: Node[Any] => DefaultMutableTreeNode)
   1.103    {
   1.104      for ((_, (node, subtree)) <- branches) {
   1.105        val current = swing_node(node)