--- a/src/Tools/jEdit/src/prover/MarkupNode.scala Sun Feb 01 13:57:59 2009 +0100
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala Mon Feb 02 23:05:25 2009 +0100
@@ -94,12 +94,12 @@
val filled_gaps = for {
child <- children
markups = if (next_x < child.start) {
- new MarkupNode(base, next_x, child.start, id, kind, desc) :: child.flatten
+ new MarkupNode(base, next_x, child.start, id, kind, "") :: child.flatten
} else child.flatten
update = (next_x = child.stop)
markup <- markups
} yield markup
- if (next_x <= stop) filled_gaps + new MarkupNode(base, next_x, stop, id, kind, desc)
+ if (next_x < stop) filled_gaps + new MarkupNode(base, next_x, stop, id, kind, "")
else filled_gaps
}
}
@@ -131,4 +131,5 @@
def fitting_into(node : MarkupNode) = node.start <= this.start &&
node.stop >= this.stop
+ override def toString = "([" + start + " - " + stop + "] " + id + "( " + kind + "): " + desc
}