--- a/src/Tools/jEdit/src/prover/MarkupNode.scala Wed Dec 10 14:45:04 2008 +0100
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala Wed Dec 10 19:51:15 2008 +0100
@@ -66,7 +66,12 @@
private def remove(nodes : List[MarkupNode]) {
children_cell = children diff nodes
- for(node <- nodes) swing_node remove node.swing_node
+ for(node <- nodes) try {
+ swing_node remove node.swing_node
+ } catch { case e : IllegalArgumentException =>
+ System.err.println(e.toString)
+ case e => throw e
+ }
}
def dfs : List[MarkupNode] = {