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