# HG changeset patch # User immler@in.tum.de # Date 1228759866 -3600 # Node ID 1b61a92f867503015b29b9214d3fcd06be731bd7 # Parent 5b8b89b7e5974a5328f58d1693086e0a335c5054 MarkupNode instead of DefaultMutableTreeNode and RelativeAsset diff -r 5b8b89b7e597 -r 1b61a92f8675 src/Tools/jEdit/src/jedit/TheoryView.scala --- a/src/Tools/jEdit/src/jedit/TheoryView.scala Sun Dec 07 19:55:01 2008 +0100 +++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Mon Dec 08 19:11:06 2008 +0100 @@ -204,12 +204,11 @@ // paint details of command var nodes = e.root_node.breadthFirstEnumeration while(nodes.hasMoreElements){ - val node = nodes.nextElement.asInstanceOf[javax.swing.tree.DefaultMutableTreeNode] - val node_asset = node.getUserObject.asInstanceOf[isabelle.prover.RelativeAsset] - val begin = toCurrent(node_asset.rel_start + e.start) - val finish = toCurrent(node_asset.rel_end + e.start) + val node = nodes.nextElement.asInstanceOf[isabelle.prover.MarkupNode] + val begin = toCurrent(node.rel_start + e.start) + val finish = toCurrent(node.rel_end + e.start) if(finish > start && begin < end) - encolor(gfx, y + fm.getHeight - 4, 2, begin max start, finish min end, chooseColor(node_asset.getShortDescription), true) + encolor(gfx, y + fm.getHeight - 4, 2, begin max start, finish min end, chooseColor(node.short), true) } e = e.next } diff -r 5b8b89b7e597 -r 1b61a92f8675 src/Tools/jEdit/src/prover/Command.scala --- a/src/Tools/jEdit/src/prover/Command.scala Sun Dec 07 19:55:01 2008 +0100 +++ b/src/Tools/jEdit/src/prover/Command.scala Mon Dec 08 19:11:06 2008 +0100 @@ -3,8 +3,7 @@ import isabelle.proofdocument.Token import isabelle.jedit.Plugin import isabelle.{ YXML, XML } -import sidekick.{SideKickParsedData} -import sidekick.enhanced.SourceAsset +import sidekick.{SideKickParsedData, IAsset} import javax.swing.text.Position import javax.swing.tree.DefaultMutableTreeNode @@ -67,51 +66,12 @@ results = results ::: List(tree) } - val root_node = { - val content = document.getContent(this) - val ra = new RelativeAsset(this, 0, stop - start, "Command", content) - new DefaultMutableTreeNode(ra) - } - - // does cand fit into node? - private def fitting(cand : DefaultMutableTreeNode, node : DefaultMutableTreeNode) : boolean = { - val node_asset = node.getUserObject.asInstanceOf[RelativeAsset] - val n_start = node_asset.rel_start - val n_end = node_asset.rel_end - val cand_asset = cand.getUserObject.asInstanceOf[RelativeAsset] - val c_start = cand_asset.rel_start - val c_end = cand_asset.rel_end - return c_start >= n_start && c_end <= n_end - } + val root_node = + new MarkupNode(this, 0, stop - start, idString, "Command", document.getContent(this)) - private def insert_node(new_node : DefaultMutableTreeNode, node : DefaultMutableTreeNode) { - assert(fitting(new_node, node)) - val children = node.children - while (children.hasMoreElements){ - val child = children.nextElement.asInstanceOf[DefaultMutableTreeNode] - if(fitting(new_node, child)) { - insert_node(new_node, child) - } - } - if(new_node.getParent == null){ - while(children.hasMoreElements){ - val child = children.nextElement.asInstanceOf[DefaultMutableTreeNode] - if(fitting(child, new_node)) { - node.remove(child.asInstanceOf[DefaultMutableTreeNode]) - new_node.add(child) - } - } - node.add(new_node) - } - } - - def add_node(node : DefaultMutableTreeNode) = insert_node(node, root_node) - - def node_from(kind : String, begin : Int, end : Int) : DefaultMutableTreeNode = { - val markup_content = /*content.substring(begin, end)*/ - "" - val asset = new RelativeAsset(this, begin, end, kind, markup_content) - new DefaultMutableTreeNode(asset) + def node_from(kind : String, begin : Int, end : Int) : MarkupNode = { + val markup_content = /*content.substring(begin, end)*/ "" + new MarkupNode(this, begin, end, idString, kind, markup_content) } def content = document.getContent(this) diff -r 5b8b89b7e597 -r 1b61a92f8675 src/Tools/jEdit/src/prover/MarkupNode.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/prover/MarkupNode.scala Mon Dec 08 19:11:06 2008 +0100 @@ -0,0 +1,76 @@ +/* + * RelativeAsset.scala + * + * To change this template, choose Tools | Template Manager + * and open the template in the editor. + */ + +package isabelle.prover + +import sidekick.IAsset +import javax.swing._ +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{ + + private class MyPos(val o : Int) extends Position { + override def getOffset = o + } + + private def pos(x : Int) : MyPos = new MyPos(x) + + 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 + } + + super.setUserObject(RelativeAsset) + + 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) + } + } + 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 + ")") + } + } else { + super.add(new_child) + } + } + + // does node fit into this? + def fitting(node : MarkupNode) : boolean = { + return node.rel_start >= this.rel_start && node.rel_end <= this.rel_end + } + +} diff -r 5b8b89b7e597 -r 1b61a92f8675 src/Tools/jEdit/src/prover/Prover.scala --- a/src/Tools/jEdit/src/prover/Prover.scala Sun Dec 07 19:55:01 2008 +0100 +++ b/src/Tools/jEdit/src/prover/Prover.scala Mon Dec 08 19:11:06 2008 +0100 @@ -82,7 +82,7 @@ if(st == null) commands.getOrElse(id, null) // inner syntax: id from props else st - command.add_node(command.node_from(kind, begin, end)) + command.root_node.add(command.node_from(kind, begin, end)) // Phase changed case Elem("finished", _, _) => st.phase = Phase.FINISHED diff -r 5b8b89b7e597 -r 1b61a92f8675 src/Tools/jEdit/src/prover/RelativeAsset.scala --- a/src/Tools/jEdit/src/prover/RelativeAsset.scala Sun Dec 07 19:55:01 2008 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,48 +0,0 @@ -/* - * RelativeAsset.scala - * - * To change this template, choose Tools | Template Manager - * and open the template in the editor. - */ - -package isabelle.prover - -import sidekick.enhanced.SourceAsset -import javax.swing._ -import javax.swing.text.Position - -class RelativeAsset(base : Command, var rel_start : Int, var rel_end : Int, cons_name : String, desc : String) - extends SourceAsset { - -class MyPos(val o : Int) extends Position { - override def getOffset = o -} - { - setStart(new MyPos(base.start + rel_start)) - setEnd(new MyPos(base.start + rel_end)) - setName(cons_name) - setShort(cons_name) - setLong(desc) - - } - /** - * Set the start position - */ - override def setStart(start : Position) { rel_start = start.getOffset - base.start } - - /** - * Returns the starting position. - */ - override def getStart : Position = new MyPos(base.start + rel_start) - - /** - * Set the end position - */ - override def setEnd(end : Position) { rel_end = end.getOffset - base.start } - - /** - * Returns the end position. - */ - override def getEnd : Position = new MyPos(base.start + rel_end) - -}