--- a/src/Tools/jEdit/src/prover/MarkupNode.scala Thu Aug 27 10:51:09 2009 +0200
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala Thu Aug 27 10:51:09 2009 +0200
@@ -15,8 +15,6 @@
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
@@ -56,9 +54,6 @@
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))