src/Tools/jEdit/src/prover/MarkupNode.scala

 import javax.swing.text.Position
 import javax.swing.tree._
 
 abstract class MarkupInfo
 case class RootInfo() extends MarkupInfo
-case class OuterInfo(highlight: String) extends
-  MarkupInfo { override def toString = highlight }
 case class HighlightInfo(highlight: String) extends
   MarkupInfo { override def toString = highlight }
 case class TypeInfo(type_kind: String) extends
   MarkupInfo { override def toString = type_kind }
 case class RefInfo(file: Option[String], line: Option[Int],

 
 class MarkupNode(val base: Command, val start: Int, val stop: Int,
   val children: List[MarkupNode],
   val id: String, val content: String, val info: MarkupInfo)
 {
-
-  def transform(f: Int => Int): MarkupNode = new MarkupNode(base,
-    f(start), f(stop), children map (_ transform f), id, content, info)
 
   def swing_node(doc: ProofDocument): DefaultMutableTreeNode = {
     val node = MarkupNode.markup2default_node (this, base, doc)
     children.map(node add _.swing_node(doc))
     node