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