--- 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
}
--- 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)
--- /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
+ }
+
+}
--- 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
--- 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)
-
-}