changeset 34597 | a0c84b0edb9a |
parent 34582 | 5d5d253c7c29 |
parent 34590 | 320b33f30cae |
child 34656 | 2740439a86b4 |
--- a/src/Tools/jEdit/src/prover/MarkupNode.scala Tue Jun 02 22:00:28 2009 +0200 +++ b/src/Tools/jEdit/src/prover/MarkupNode.scala Tue Jun 02 22:55:13 2009 +0200 @@ -125,8 +125,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 } }