# HG changeset patch # User immler@in.tum.de # Date 1228916704 -3600 # Node ID 44241a37b74a3450c8e5bfc5261762851826b29e # Parent 1b61a92f867503015b29b9214d3fcd06be731bd7 structure of markup-tree in scala, keep track of swing-nodes in background diff -r 1b61a92f8675 -r 44241a37b74a src/Tools/jEdit/src/jedit/TheoryView.scala --- a/src/Tools/jEdit/src/jedit/TheoryView.scala Mon Dec 08 19:11:06 2008 +0100 +++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Wed Dec 10 14:45:04 2008 +0100 @@ -202,11 +202,9 @@ val finish = end - 1 min toCurrent(e.stop) encolor(gfx, y, fm.getHeight, begin, finish, chooseColor(e), true) // paint details of command - var nodes = e.root_node.breadthFirstEnumeration - while(nodes.hasMoreElements){ - val node = nodes.nextElement.asInstanceOf[isabelle.prover.MarkupNode] - val begin = toCurrent(node.rel_start + e.start) - val finish = toCurrent(node.rel_end + e.start) + for(node <- e.root_node.dfs){ + val begin = toCurrent(node.start + e.start) + val finish = toCurrent(node.end + e.start) if(finish > start && begin < end) encolor(gfx, y + fm.getHeight - 4, 2, begin max start, finish min end, chooseColor(node.short), true) } diff -r 1b61a92f8675 -r 44241a37b74a src/Tools/jEdit/src/prover/Command.scala --- a/src/Tools/jEdit/src/prover/Command.scala Mon Dec 08 19:11:06 2008 +0100 +++ b/src/Tools/jEdit/src/prover/Command.scala Wed Dec 10 14:45:04 2008 +0100 @@ -43,10 +43,8 @@ def phase_=(p_new : Phase.Value) = { if(p_new == Phase.UNPROCESSED){ //delete inner syntax - val children = root_node.children - while (children.hasMoreElements){ - val child = children.nextElement.asInstanceOf[DefaultMutableTreeNode] - child.removeAllChildren + for(child <- root_node.children){ + child.children = Nil } } p = p_new diff -r 1b61a92f8675 -r 44241a37b74a src/Tools/jEdit/src/prover/IsabelleSKParser.scala --- a/src/Tools/jEdit/src/prover/IsabelleSKParser.scala Mon Dec 08 19:11:06 2008 +0100 +++ b/src/Tools/jEdit/src/prover/IsabelleSKParser.scala Wed Dec 10 14:45:04 2008 +0100 @@ -31,9 +31,9 @@ val buffer = Plugin.plugin.theoryView.buffer.asInstanceOf[Buffer] val document = prover.document val data = new SideKickParsedData(buffer.getPath) - //TODO: catch npe s + for(command <- document.commands){ - data.root.add(command.root_node) + data.root.add(command.root_node.swing_node) } data } diff -r 1b61a92f8675 -r 44241a37b74a src/Tools/jEdit/src/prover/MarkupNode.scala --- a/src/Tools/jEdit/src/prover/MarkupNode.scala Mon Dec 08 19:11:06 2008 +0100 +++ b/src/Tools/jEdit/src/prover/MarkupNode.scala Wed Dec 10 14:45:04 2008 +0100 @@ -12,65 +12,96 @@ import javax.swing.text.Position import javax.swing.tree._ -class MarkupNode (base : Command, val rel_start : Int, val rel_end : Int, - val name : String, val short : String, val long : String) - extends DefaultMutableTreeNode{ +object MarkupNode { + + def markup2default_node(node : MarkupNode) : DefaultMutableTreeNode = { + + class MyPos(val o : Int) extends Position { + override def getOffset = o + } + + implicit def int2pos(x : Int) : MyPos = new MyPos(x) - private class MyPos(val o : Int) extends Position { - override def getOffset = o - } - - private def pos(x : Int) : MyPos = new MyPos(x) + object RelativeAsset extends IAsset{ + override def getIcon : Icon = null + override def getShortString : String = node.short + override def getLongString : String = node.long + override def getName : String = node.name + override def setName (name : String) = () + override def setStart(start : Position) = () + override def getStart : Position = node.base.start + node.start + override def setEnd(end : Position) = () + override def getEnd : Position = node.base.start + node.end + override def toString = node.name + ": " + node.short + } - private object RelativeAsset extends IAsset{ - override def getIcon : Icon = null - override def getShortString : String = short - override def getLongString : String = long - override def getName : String = name - override def setName (name : String) = () - override def setStart(start : Position) = () - override def getStart : Position = pos(base.start + rel_start) - override def setEnd(end : Position) = () - override def getEnd : Position = pos(base.start + rel_end) - override def toString = name + ": " + short + new DefaultMutableTreeNode(RelativeAsset) + } +} + +class MarkupNode (val base : Command, val start : Int, val end : Int, + val name : String, val short : String, val long : String) { + + val swing_node : DefaultMutableTreeNode = MarkupNode.markup2default_node (this) + + var parent : MarkupNode = null + def orphan = parent == null + + private var children_cell : List[MarkupNode] = Nil + //track changes in swing_node + def children = children_cell + def children_= (cs : List[MarkupNode]) = { + swing_node.removeAllChildren + for(c <- cs) swing_node add c.swing_node + children_cell = cs + } + + private def add(child : MarkupNode) { + child parent = this + children_cell = (child :: children) sort ((a, b) => a.start < b.end) + + swing_node add child.swing_node } - super.setUserObject(RelativeAsset) + private def remove(nodes : List[MarkupNode]) { + children_cell = children diff nodes + + for(node <- nodes) swing_node remove node.swing_node + } - override def add(new_child : MutableTreeNode) = { - if(new_child.isInstanceOf[MarkupNode]){ - val new_node = new_child.asInstanceOf[MarkupNode] - if(!equals(new_node) && fitting(new_node)){ - val cs = children() - while (cs.hasMoreElements){ - val child = cs.nextElement.asInstanceOf[MarkupNode] - if(child.fitting(new_node)) { - child.add(new_node) + def dfs : List[MarkupNode] = { + var all = Nil : List[MarkupNode] + for(child <- children) + all = child.dfs ::: all + all = this :: all + all + } + + def insert(new_child : MarkupNode) : Unit = { + if(new_child fitting_into this){ + for(child <- children){ + if(new_child fitting_into child) + child insert new_child + } + if(new_child orphan){ + // new_child did not fit into children of this + // -> insert new_child between this and its children + for(child <- children){ + if(child fitting_into new_child) { + new_child add child } } - if(new_node.getParent == null){ - val cs = children() - while(cs.hasMoreElements){ - val child = cs.nextElement.asInstanceOf[MarkupNode] - if(new_node.fitting(child)) { - remove(child) - new_node.add(child) - } - } - super.add(new_node) - } - } else { - System.err.println("ignored nonfitting markup " + new_node.name + new_node.short + new_node.long - + "(" +new_node.rel_start + ", "+ new_node.rel_end + ")") + this add new_child + this remove new_child.children } } else { - super.add(new_child) + System.err.println("ignored nonfitting markup " + new_child.name + new_child.short + new_child.long + + "(" +new_child.start + ", "+ new_child.end + ")") } } - // does node fit into this? - def fitting(node : MarkupNode) : boolean = { - return node.rel_start >= this.rel_start && node.rel_end <= this.rel_end - } + // does this fit into node? + def fitting_into(node : MarkupNode) = node.start <= this.start && + node.end >= this.end } diff -r 1b61a92f8675 -r 44241a37b74a src/Tools/jEdit/src/prover/Prover.scala --- a/src/Tools/jEdit/src/prover/Prover.scala Mon Dec 08 19:11:06 2008 +0100 +++ b/src/Tools/jEdit/src/prover/Prover.scala Wed Dec 10 14:45:04 2008 +0100 @@ -82,7 +82,7 @@ if(st == null) commands.getOrElse(id, null) // inner syntax: id from props else st - command.root_node.add(command.node_from(kind, begin, end)) + command.root_node.insert(command.node_from(kind, begin, end)) // Phase changed case Elem("finished", _, _) => st.phase = Phase.FINISHED