src/Pure/PIDE/markup_tree.scala

--- a/src/Pure/PIDE/markup_tree.scala	Fri Nov 11 14:07:20 2011 +0100
+++ b/src/Pure/PIDE/markup_tree.scala	Fri Nov 11 14:24:38 2011 +0100
@@ -19,7 +19,7 @@
 
   object Branches
   {
-    type Entry = (Text.Info[Any], Markup_Tree)
+    type Entry = (Text.Markup, Markup_Tree)
     type T = SortedMap[Text.Range, Entry]
 
     val empty = SortedMap.empty[Text.Range, Entry](Text.Range.Ordering)
@@ -41,7 +41,7 @@
 
   val empty = new Markup_Tree(Branches.empty)
 
-  type Select[A] = PartialFunction[Text.Info[Any], A]
+  type Select[A] = PartialFunction[Text.Markup, A]
 }
 
 
@@ -55,7 +55,7 @@
       case list => list.mkString("Tree(", ",", ")")
     }
 
-  def + (new_info: Text.Info[Any]): Markup_Tree =
+  def + (new_info: Text.Markup): Markup_Tree =
   {
     val new_range = new_info.range
     branches.get(new_range) match {
@@ -126,7 +126,7 @@
   }
 
   def swing_tree(parent: DefaultMutableTreeNode)
-    (swing_node: Text.Info[Any] => DefaultMutableTreeNode)
+    (swing_node: Text.Markup => DefaultMutableTreeNode)
   {
     for ((_, (info, subtree)) <- branches) {
       val current = swing_node(info)