--- a/src/Tools/jEdit/src/prover/MarkupNode.scala Sun Sep 06 16:21:01 2009 +0200
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala Sun Sep 06 22:27:32 2009 +0200
@@ -12,78 +12,100 @@
import isabelle.proofdocument.ProofDocument
-class MarkupNode(val start: Int, val stop: Int, val content: String, val info: Any,
- val children: List[MarkupNode])
+class Markup_Node(val start: Int, val stop: Int, val info: Any)
{
+ def fits_into(that: Markup_Node): Boolean =
+ that.start <= this.start && this.stop <= that.stop
+}
+
- def swing_tree(make_node: MarkupNode => DefaultMutableTreeNode): DefaultMutableTreeNode =
- {
- val node = make_node(this)
- children.foreach(node add _.swing_tree(make_node))
- node
- }
+class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree])
+{
+ def set_branches(bs: List[Markup_Tree]): Markup_Tree = new Markup_Tree(node, bs)
- def set_children(new_children: List[MarkupNode]): MarkupNode =
- new MarkupNode(start, stop, content, info, new_children)
+ private def add(branch: Markup_Tree) = // FIXME avoid sort
+ set_branches((branch :: branches) sort ((a, b) => a.node.start < b.node.start))
- private def add(child: MarkupNode) = // FIXME avoid sort?
- set_children ((child :: children) sort ((a, b) => a.start < b.start))
-
- def remove(nodes: List[MarkupNode]) = set_children(children -- nodes)
+ private def remove(bs: List[Markup_Tree]) = set_branches(branches -- bs)
- def fits_into(node: MarkupNode): Boolean =
- node.start <= this.start && this.stop <= node.stop
-
- def + (new_child: MarkupNode): MarkupNode =
+ def + (new_tree: Markup_Tree): Markup_Tree =
{
- if (new_child fits_into this) {
+ val new_node = new_tree.node
+ if (new_node fits_into node) {
var inserted = false
- val new_children =
- children.map(c =>
- if ((new_child fits_into c) && !inserted) {inserted = true; c + new_child}
- else c)
+ val new_branches =
+ branches.map(branch =>
+ if ((new_node fits_into branch.node) && !inserted) {
+ inserted = true
+ branch + new_tree
+ }
+ else branch)
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) (_ + _))
+ // new_tree did not fit into children of this
+ // -> insert between this and its branches
+ val fitting = branches filter(_.node fits_into new_node)
+ (this remove fitting) add ((new_tree /: fitting)(_ + _))
}
- else this set_children new_children
+ else set_branches(new_branches)
}
else {
- System.err.println("ignored nonfitting markup: " + new_child)
+ System.err.println("ignored nonfitting markup: " + new_node)
this
}
}
- def flatten: List[MarkupNode] = {
- var next_x = start
- if (children.isEmpty) List(this)
+ def flatten: List[Markup_Node] =
+ {
+ var next_x = node.start
+ if (branches.isEmpty) List(this.node)
else {
- val filled_gaps = for {
- child <- children
- markups =
- if (next_x < child.start) {
- // FIXME proper content!?
- new MarkupNode(next_x, child.start, content, info, Nil) :: child.flatten
- }
- else child.flatten
- update = (next_x = child.stop)
- markup <- markups
- } yield markup
- if (next_x < stop)
- filled_gaps + new MarkupNode(next_x, stop, content, info, Nil) // FIXME proper content!?
+ val filled_gaps =
+ for {
+ child <- branches
+ markups =
+ if (next_x < child.node.start)
+ new Markup_Node(next_x, child.node.start, node.info) :: child.flatten
+ else child.flatten
+ update = (next_x = child.node.stop)
+ markup <- markups
+ } yield markup
+ if (next_x < node.stop)
+ filled_gaps + new Markup_Node(next_x, node.stop, node.info)
else filled_gaps
}
}
+}
- def filter(p: MarkupNode => Boolean): List[MarkupNode] =
+
+class Markup_Text(val markup: List[Markup_Tree], val content: String)
+{
+ private lazy val root =
+ new Markup_Tree(new Markup_Node(0, content.length, None), markup)
+
+ def + (new_tree: Markup_Tree): Markup_Text =
+ new Markup_Text((root + new_tree).branches, content)
+
+ def filter(pred: Markup_Node => Boolean): Markup_Text =
{
- val filtered = children.flatMap(_.filter(p))
- if (p(this)) List(this set_children(filtered))
- else filtered
+ def filt(tree: Markup_Tree): List[Markup_Tree] =
+ {
+ val branches = tree.branches.flatMap(filt(_))
+ if (pred(tree.node)) List(tree.set_branches(branches))
+ else branches
+ }
+ new Markup_Text(markup.flatMap(filt(_)), content)
}
- override def toString =
- "([" + start + " - " + stop + "] ( " + content + "): " + info.toString
+ def flatten: List[Markup_Node] = markup.flatten(_.flatten)
+
+ def swing_tree(swing_node: Markup_Node => DefaultMutableTreeNode): DefaultMutableTreeNode =
+ {
+ def swing(tree: Markup_Tree): DefaultMutableTreeNode =
+ {
+ val node = swing_node(tree.node)
+ tree.branches foreach ((branch: Markup_Tree) => node.add(swing(branch)))
+ node
+ }
+ swing(root)
+ }
}