src/Pure/PIDE/markup_tree.scala
changeset 45455 4f974c0c5c2f
parent 44379 1079ab6b342b
child 45456 9ba615ac75fb
     1.1 --- a/src/Pure/PIDE/markup_tree.scala	Fri Nov 11 14:07:20 2011 +0100
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Fri Nov 11 14:24:38 2011 +0100
     1.3 @@ -19,7 +19,7 @@
     1.4  
     1.5    object Branches
     1.6    {
     1.7 -    type Entry = (Text.Info[Any], Markup_Tree)
     1.8 +    type Entry = (Text.Markup, Markup_Tree)
     1.9      type T = SortedMap[Text.Range, Entry]
    1.10  
    1.11      val empty = SortedMap.empty[Text.Range, Entry](Text.Range.Ordering)
    1.12 @@ -41,7 +41,7 @@
    1.13  
    1.14    val empty = new Markup_Tree(Branches.empty)
    1.15  
    1.16 -  type Select[A] = PartialFunction[Text.Info[Any], A]
    1.17 +  type Select[A] = PartialFunction[Text.Markup, A]
    1.18  }
    1.19  
    1.20  
    1.21 @@ -55,7 +55,7 @@
    1.22        case list => list.mkString("Tree(", ",", ")")
    1.23      }
    1.24  
    1.25 -  def + (new_info: Text.Info[Any]): Markup_Tree =
    1.26 +  def + (new_info: Text.Markup): Markup_Tree =
    1.27    {
    1.28      val new_range = new_info.range
    1.29      branches.get(new_range) match {
    1.30 @@ -126,7 +126,7 @@
    1.31    }
    1.32  
    1.33    def swing_tree(parent: DefaultMutableTreeNode)
    1.34 -    (swing_node: Text.Info[Any] => DefaultMutableTreeNode)
    1.35 +    (swing_node: Text.Markup => DefaultMutableTreeNode)
    1.36    {
    1.37      for ((_, (info, subtree)) <- branches) {
    1.38        val current = swing_node(info)