--- a/src/Tools/jEdit/src/prover/MarkupNode.scala Thu Sep 03 20:10:23 2009 +0200
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala Fri Sep 04 23:04:20 2009 +0200
@@ -49,6 +49,31 @@
def remove(nodes: List[MarkupNode]) = set_children(children diff nodes)
+ def fits_into(node: MarkupNode): Boolean =
+ node.start <= this.start && this.stop <= node.stop
+
+ def + (new_child: MarkupNode): MarkupNode =
+ {
+ if (new_child fits_into this) {
+ var inserted = false
+ val new_children =
+ children.map(c =>
+ if ((new_child fits_into c) && !inserted) {inserted = true; c + new_child}
+ else c)
+ if (!inserted) {
+ // new_child did not fit into children of this
+ // -> insert new_child between this and its children
+ val fitting = children filter(_ fits_into new_child)
+ (this remove fitting) add ((new_child /: fitting) (_ + _))
+ }
+ else this set_children new_children
+ }
+ else {
+ System.err.println("ignored nonfitting markup: " + new_child)
+ this
+ }
+ }
+
def dfs: List[MarkupNode] = {
var all = Nil : List[MarkupNode]
for (child <- children)
@@ -59,13 +84,13 @@
def leafs: List[MarkupNode] =
{
- if (children == Nil) return List(this)
+ if (children.isEmpty) return List(this)
else return children flatMap (_.leafs)
}
def flatten: List[MarkupNode] = {
var next_x = start
- if(children.length == 0) List(this)
+ if (children.isEmpty) List(this)
else {
val filled_gaps = for {
child <- children
@@ -89,31 +114,6 @@
else filtered
}
- def + (new_child: MarkupNode): MarkupNode =
- {
- if (new_child fitting_into this) {
- var inserted = false
- val new_children =
- children.map(c =>
- if ((new_child fitting_into c) && !inserted) {inserted = true; c + new_child}
- else c)
- if (!inserted) {
- // new_child did not fit into children of this
- // -> insert new_child between this and its children
- val fitting = children filter(_ fitting_into new_child)
- (this remove fitting) add ((new_child /: fitting) (_ + _))
- }
- else this set_children new_children
- }
- else {
- System.err.println("ignored nonfitting markup: " + new_child)
- this
- }
- }
-
- // does this fit into node?
- def fitting_into(node: MarkupNode) = node.start <= this.start && node.stop >= this.stop
-
override def toString =
"([" + start + " - " + stop + "] " + id + "( " + content + "): " + info.toString
}