# HG changeset patch
# User immler@in.tum.de
# Date 1243962058 -7200
# Node ID 320b33f30cae28bfb68bd3b68efeb1d30578b14b
# Parent  abab3a577e10c400c02bb06b777f83b6541a3a69
return unchanged node on errors

diff -r abab3a577e10 -r 320b33f30cae src/Tools/jEdit/src/prover/MarkupNode.scala
--- 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
     }
   }