# HG changeset patch
# User immler@in.tum.de
# Date 1249311393 -7200
# Node ID e888d0cdda9c3ff2a500503d94d1fedb61067bd9
# Parent  3b05426b93186006718832ca1f0c4c7bbae54228
add is a private function

diff -r 3b05426b9318 -r e888d0cdda9c src/Tools/jEdit/src/prover/MarkupNode.scala
--- 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)