--- a/src/Tools/jEdit/src/prover/MarkupNode.scala Wed Jul 15 13:13:09 2009 +0200
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala Wed Jul 15 13:49:21 2009 +0200
@@ -55,6 +55,10 @@
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))