return unchanged node on errors

--- a/src/Tools/jEdit/src/prover/MarkupNode.scala	Sat May 30 23:27:37 2009 +0200
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala	Tue Jun 02 19:00:58 2009 +0200
@@ -114,8 +114,8 @@
       }
       else this set_children new_children
     } else {
-      error("ignored nonfitting markup " + new_child.id + new_child.content + new_child.info.toString
-                         + "(" +new_child.start + ", "+ new_child.stop + ")")
+      System.err.println("ignored nonfitting markup: " + new_child)
+      this
     }
   }