src/Tools/jEdit/src/prover/MarkupNode.scala
author wenzelm
Mon, 19 Jan 2009 15:56:58 +0100
changeset 34480 017fae24829f
parent 34407 aad6834ba380
child 34503 7d0726f19d04
permissions -rw-r--r--
simplified implicit convertion Int => Position;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
     1
/*
34407
aad6834ba380 added some headers and comments;
wenzelm
parents: 34402
diff changeset
     2
 * Document markup nodes, with connection to Swing tree model
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
     3
 *
34407
aad6834ba380 added some headers and comments;
wenzelm
parents: 34402
diff changeset
     4
 * @author Fabian Immler, TU Munich
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
     5
 */
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
     6
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
     7
package isabelle.prover
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
     8
34400
1b61a92f8675 MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents: 34393
diff changeset
     9
import sidekick.IAsset
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
    10
import javax.swing._
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
    11
import javax.swing.text.Position
34400
1b61a92f8675 MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents: 34393
diff changeset
    12
import javax.swing.tree._
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
    13
34401
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    14
object MarkupNode {
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    15
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    16
  def markup2default_node(node : MarkupNode) : DefaultMutableTreeNode = {
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    17
34480
017fae24829f simplified implicit convertion Int => Position;
wenzelm
parents: 34407
diff changeset
    18
    implicit def int2pos(offset: Int): Position =
017fae24829f simplified implicit convertion Int => Position;
wenzelm
parents: 34407
diff changeset
    19
      new Position { def getOffset = offset }
34401
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    20
34480
017fae24829f simplified implicit convertion Int => Position;
wenzelm
parents: 34407
diff changeset
    21
    object RelativeAsset extends IAsset {
34401
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    22
      override def getIcon : Icon = null
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    23
      override def getShortString : String = node.short
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    24
      override def getLongString : String = node.long
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    25
      override def getName : String = node.name
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    26
      override def setName (name : String) = ()
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    27
      override def setStart(start : Position) = ()
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    28
      override def getStart : Position = node.base.start + node.start
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    29
      override def setEnd(end : Position) = ()
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    30
      override def getEnd : Position = node.base.start + node.end
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    31
      override def toString = node.name + ": " + node.short
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    32
    }
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
    33
34401
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    34
    new DefaultMutableTreeNode(RelativeAsset)
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    35
  }
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    36
}
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    37
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    38
class MarkupNode (val base : Command, val start : Int, val end : Int,
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    39
                    val name : String, val short : String, val long : String) {
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    40
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    41
  val swing_node : DefaultMutableTreeNode = MarkupNode.markup2default_node (this)
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    42
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    43
  var parent : MarkupNode = null
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    44
  def orphan = parent == null
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    45
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    46
  private var children_cell : List[MarkupNode] = Nil
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    47
  //track changes in swing_node
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    48
  def children = children_cell
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    49
  def children_= (cs : List[MarkupNode]) = {
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    50
    swing_node.removeAllChildren
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    51
    for(c <- cs) swing_node add c.swing_node
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    52
    children_cell = cs
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    53
  }
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    54
  
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    55
  private def add(child : MarkupNode) {
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    56
    child parent = this
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    57
    children_cell = (child :: children) sort ((a, b) => a.start < b.end)
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    58
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    59
    swing_node add child.swing_node
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
    60
  }
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
    61
34401
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    62
  private def remove(nodes : List[MarkupNode]) {
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    63
    children_cell = children diff nodes
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    64
34402
bd8d70cd9baf information on command-phase left of scrollbar
immler@in.tum.de
parents: 34401
diff changeset
    65
      for(node <- nodes) try {
bd8d70cd9baf information on command-phase left of scrollbar
immler@in.tum.de
parents: 34401
diff changeset
    66
        swing_node remove node.swing_node
bd8d70cd9baf information on command-phase left of scrollbar
immler@in.tum.de
parents: 34401
diff changeset
    67
      } catch { case e : IllegalArgumentException =>
bd8d70cd9baf information on command-phase left of scrollbar
immler@in.tum.de
parents: 34401
diff changeset
    68
        System.err.println(e.toString)
bd8d70cd9baf information on command-phase left of scrollbar
immler@in.tum.de
parents: 34401
diff changeset
    69
        case e => throw e
bd8d70cd9baf information on command-phase left of scrollbar
immler@in.tum.de
parents: 34401
diff changeset
    70
      }
34401
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    71
  }
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
    72
34401
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    73
  def dfs : List[MarkupNode] = {
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    74
    var all = Nil : List[MarkupNode]
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    75
    for(child <- children)
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    76
      all = child.dfs ::: all
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    77
    all = this :: all
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    78
    all
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    79
  }
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    80
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    81
  def insert(new_child : MarkupNode) : Unit = {
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    82
    if(new_child fitting_into this){
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    83
      for(child <- children){
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    84
        if(new_child fitting_into child)
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    85
          child insert new_child
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    86
      }
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    87
      if(new_child orphan){
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    88
        // new_child did not fit into children of this
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    89
        // -> insert new_child between this and its children
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    90
        for(child <- children){
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    91
          if(child fitting_into new_child) {
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    92
            new_child add child
34400
1b61a92f8675 MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents: 34393
diff changeset
    93
          }
1b61a92f8675 MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents: 34393
diff changeset
    94
        }
34401
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    95
        this add new_child
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    96
        this remove new_child.children
34400
1b61a92f8675 MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents: 34393
diff changeset
    97
      }
1b61a92f8675 MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents: 34393
diff changeset
    98
    } else {
34401
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    99
      System.err.println("ignored nonfitting markup " + new_child.name + new_child.short + new_child.long
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
   100
                         + "(" +new_child.start + ", "+ new_child.end + ")")
34400
1b61a92f8675 MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents: 34393
diff changeset
   101
    }
1b61a92f8675 MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents: 34393
diff changeset
   102
  }
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
   103
34401
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
   104
  // does this fit into node?
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
   105
  def fitting_into(node : MarkupNode) = node.start <= this.start &&
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
   106
    node.end >= this.end
34400
1b61a92f8675 MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents: 34393
diff changeset
   107
  
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
   108
}