1.1 --- a/src/Tools/jEdit/src/prover/MarkupNode.scala Sun Sep 06 16:21:01 2009 +0200
1.2 +++ b/src/Tools/jEdit/src/prover/MarkupNode.scala Sun Sep 06 22:27:32 2009 +0200
1.3 @@ -12,78 +12,100 @@
1.4 import isabelle.proofdocument.ProofDocument
1.5
1.6
1.7 -class MarkupNode(val start: Int, val stop: Int, val content: String, val info: Any,
1.8 - val children: List[MarkupNode])
1.9 +class Markup_Node(val start: Int, val stop: Int, val info: Any)
1.10 {
1.11 + def fits_into(that: Markup_Node): Boolean =
1.12 + that.start <= this.start && this.stop <= that.stop
1.13 +}
1.14 +
1.15
1.16 - def swing_tree(make_node: MarkupNode => DefaultMutableTreeNode): DefaultMutableTreeNode =
1.17 - {
1.18 - val node = make_node(this)
1.19 - children.foreach(node add _.swing_tree(make_node))
1.20 - node
1.21 - }
1.22 +class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree])
1.23 +{
1.24 + def set_branches(bs: List[Markup_Tree]): Markup_Tree = new Markup_Tree(node, bs)
1.25
1.26 - def set_children(new_children: List[MarkupNode]): MarkupNode =
1.27 - new MarkupNode(start, stop, content, info, new_children)
1.28 + private def add(branch: Markup_Tree) = // FIXME avoid sort
1.29 + set_branches((branch :: branches) sort ((a, b) => a.node.start < b.node.start))
1.30
1.31 - private def add(child: MarkupNode) = // FIXME avoid sort?
1.32 - set_children ((child :: children) sort ((a, b) => a.start < b.start))
1.33 -
1.34 - def remove(nodes: List[MarkupNode]) = set_children(children -- nodes)
1.35 + private def remove(bs: List[Markup_Tree]) = set_branches(branches -- bs)
1.36
1.37 - def fits_into(node: MarkupNode): Boolean =
1.38 - node.start <= this.start && this.stop <= node.stop
1.39 -
1.40 - def + (new_child: MarkupNode): MarkupNode =
1.41 + def + (new_tree: Markup_Tree): Markup_Tree =
1.42 {
1.43 - if (new_child fits_into this) {
1.44 + val new_node = new_tree.node
1.45 + if (new_node fits_into node) {
1.46 var inserted = false
1.47 - val new_children =
1.48 - children.map(c =>
1.49 - if ((new_child fits_into c) && !inserted) {inserted = true; c + new_child}
1.50 - else c)
1.51 + val new_branches =
1.52 + branches.map(branch =>
1.53 + if ((new_node fits_into branch.node) && !inserted) {
1.54 + inserted = true
1.55 + branch + new_tree
1.56 + }
1.57 + else branch)
1.58 if (!inserted) {
1.59 - // new_child did not fit into children of this
1.60 - // -> insert new_child between this and its children
1.61 - val fitting = children filter(_ fits_into new_child)
1.62 - (this remove fitting) add ((new_child /: fitting) (_ + _))
1.63 + // new_tree did not fit into children of this
1.64 + // -> insert between this and its branches
1.65 + val fitting = branches filter(_.node fits_into new_node)
1.66 + (this remove fitting) add ((new_tree /: fitting)(_ + _))
1.67 }
1.68 - else this set_children new_children
1.69 + else set_branches(new_branches)
1.70 }
1.71 else {
1.72 - System.err.println("ignored nonfitting markup: " + new_child)
1.73 + System.err.println("ignored nonfitting markup: " + new_node)
1.74 this
1.75 }
1.76 }
1.77
1.78 - def flatten: List[MarkupNode] = {
1.79 - var next_x = start
1.80 - if (children.isEmpty) List(this)
1.81 + def flatten: List[Markup_Node] =
1.82 + {
1.83 + var next_x = node.start
1.84 + if (branches.isEmpty) List(this.node)
1.85 else {
1.86 - val filled_gaps = for {
1.87 - child <- children
1.88 - markups =
1.89 - if (next_x < child.start) {
1.90 - // FIXME proper content!?
1.91 - new MarkupNode(next_x, child.start, content, info, Nil) :: child.flatten
1.92 - }
1.93 - else child.flatten
1.94 - update = (next_x = child.stop)
1.95 - markup <- markups
1.96 - } yield markup
1.97 - if (next_x < stop)
1.98 - filled_gaps + new MarkupNode(next_x, stop, content, info, Nil) // FIXME proper content!?
1.99 + val filled_gaps =
1.100 + for {
1.101 + child <- branches
1.102 + markups =
1.103 + if (next_x < child.node.start)
1.104 + new Markup_Node(next_x, child.node.start, node.info) :: child.flatten
1.105 + else child.flatten
1.106 + update = (next_x = child.node.stop)
1.107 + markup <- markups
1.108 + } yield markup
1.109 + if (next_x < node.stop)
1.110 + filled_gaps + new Markup_Node(next_x, node.stop, node.info)
1.111 else filled_gaps
1.112 }
1.113 }
1.114 +}
1.115
1.116 - def filter(p: MarkupNode => Boolean): List[MarkupNode] =
1.117 +
1.118 +class Markup_Text(val markup: List[Markup_Tree], val content: String)
1.119 +{
1.120 + private lazy val root =
1.121 + new Markup_Tree(new Markup_Node(0, content.length, None), markup)
1.122 +
1.123 + def + (new_tree: Markup_Tree): Markup_Text =
1.124 + new Markup_Text((root + new_tree).branches, content)
1.125 +
1.126 + def filter(pred: Markup_Node => Boolean): Markup_Text =
1.127 {
1.128 - val filtered = children.flatMap(_.filter(p))
1.129 - if (p(this)) List(this set_children(filtered))
1.130 - else filtered
1.131 + def filt(tree: Markup_Tree): List[Markup_Tree] =
1.132 + {
1.133 + val branches = tree.branches.flatMap(filt(_))
1.134 + if (pred(tree.node)) List(tree.set_branches(branches))
1.135 + else branches
1.136 + }
1.137 + new Markup_Text(markup.flatMap(filt(_)), content)
1.138 }
1.139
1.140 - override def toString =
1.141 - "([" + start + " - " + stop + "] ( " + content + "): " + info.toString
1.142 + def flatten: List[Markup_Node] = markup.flatten(_.flatten)
1.143 +
1.144 + def swing_tree(swing_node: Markup_Node => DefaultMutableTreeNode): DefaultMutableTreeNode =
1.145 + {
1.146 + def swing(tree: Markup_Tree): DefaultMutableTreeNode =
1.147 + {
1.148 + val node = swing_node(tree.node)
1.149 + tree.branches foreach ((branch: Markup_Tree) => node.add(swing(branch)))
1.150 + node
1.151 + }
1.152 + swing(root)
1.153 + }
1.154 }