--- a/src/Tools/jEdit/src/prover/MarkupNode.scala Mon Jul 27 15:51:37 2009 +0200
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala Mon Aug 03 16:56:33 2009 +0200
@@ -71,7 +71,7 @@
def set_children(newchildren: List[MarkupNode]): MarkupNode =
new MarkupNode(base, start, stop, newchildren, id, content, info)
- def add(child: MarkupNode) =
+ private def add(child: MarkupNode) =
set_children ((child :: children) sort ((a, b) => a.start < b.start))
def remove(nodes: List[MarkupNode]) = set_children(children diff nodes)