src/Tools/jEdit/src/prover/MarkupNode.scala
author immler@in.tum.de
Sun Feb 01 13:32:36 2009 +0100 (2009-02-01)
changeset 34514 2104a836b415
parent 34503 7d0726f19d04
child 34517 163cda249619
permissions -rw-r--r--
renamed fields of MarkupNode; implemented flatten and leafs
immler@34393
     1
/*
wenzelm@34407
     2
 * Document markup nodes, with connection to Swing tree model
immler@34393
     3
 *
wenzelm@34407
     4
 * @author Fabian Immler, TU Munich
immler@34393
     5
 */
immler@34393
     6
immler@34393
     7
package isabelle.prover
immler@34393
     8
immler@34400
     9
import sidekick.IAsset
immler@34393
    10
import javax.swing._
immler@34393
    11
import javax.swing.text.Position
immler@34400
    12
import javax.swing.tree._
immler@34393
    13
immler@34401
    14
object MarkupNode {
immler@34401
    15
immler@34401
    16
  def markup2default_node(node : MarkupNode) : DefaultMutableTreeNode = {
immler@34401
    17
wenzelm@34480
    18
    implicit def int2pos(offset: Int): Position =
wenzelm@34480
    19
      new Position { def getOffset = offset }
immler@34401
    20
wenzelm@34480
    21
    object RelativeAsset extends IAsset {
immler@34401
    22
      override def getIcon : Icon = null
immler@34514
    23
      override def getShortString : String = node.kind
immler@34514
    24
      override def getLongString : String = node.desc
immler@34514
    25
      override def getName : String = node.id
immler@34514
    26
      override def setName (name : String) = ()
immler@34401
    27
      override def setStart(start : Position) = ()
immler@34514
    28
      override def getStart : Position = node.abs_start
immler@34401
    29
      override def setEnd(end : Position) = ()
immler@34514
    30
      override def getEnd : Position = node.abs_stop
immler@34514
    31
      override def toString = node.id + ": " + node.kind + "[" + node.start + " - " + node.stop + "]"
immler@34401
    32
    }
immler@34393
    33
immler@34401
    34
    new DefaultMutableTreeNode(RelativeAsset)
immler@34401
    35
  }
immler@34401
    36
}
immler@34401
    37
immler@34514
    38
class MarkupNode (val base : Command, val start : Int, val stop : Int,
immler@34514
    39
                    val id : String, val kind : String, val desc : String) {
immler@34401
    40
immler@34401
    41
  val swing_node : DefaultMutableTreeNode = MarkupNode.markup2default_node (this)
immler@34401
    42
immler@34401
    43
  var parent : MarkupNode = null
immler@34401
    44
  def orphan = parent == null
immler@34401
    45
immler@34514
    46
  def length = stop - start
immler@34514
    47
  def abs_start = base.start + start
immler@34514
    48
  def abs_stop = base.start + stop
immler@34514
    49
immler@34401
    50
  private var children_cell : List[MarkupNode] = Nil
immler@34401
    51
  //track changes in swing_node
immler@34401
    52
  def children = children_cell
immler@34401
    53
  def children_= (cs : List[MarkupNode]) = {
immler@34401
    54
    swing_node.removeAllChildren
wenzelm@34503
    55
    for (c <- cs) swing_node add c.swing_node
immler@34401
    56
    children_cell = cs
immler@34401
    57
  }
immler@34514
    58
immler@34401
    59
  private def add(child : MarkupNode) {
immler@34401
    60
    child parent = this
immler@34514
    61
    children_cell = (child :: children) sort ((a, b) => a.start < b.start)
immler@34401
    62
immler@34401
    63
    swing_node add child.swing_node
immler@34393
    64
  }
immler@34393
    65
immler@34401
    66
  private def remove(nodes : List[MarkupNode]) {
immler@34401
    67
    children_cell = children diff nodes
immler@34401
    68
wenzelm@34503
    69
      for (node <- nodes) try {
immler@34402
    70
        swing_node remove node.swing_node
immler@34402
    71
      } catch { case e : IllegalArgumentException =>
immler@34402
    72
        System.err.println(e.toString)
immler@34402
    73
        case e => throw e
immler@34402
    74
      }
immler@34401
    75
  }
immler@34393
    76
immler@34401
    77
  def dfs : List[MarkupNode] = {
immler@34401
    78
    var all = Nil : List[MarkupNode]
wenzelm@34503
    79
    for (child <- children)
immler@34401
    80
      all = child.dfs ::: all
immler@34401
    81
    all = this :: all
immler@34401
    82
    all
immler@34401
    83
  }
immler@34401
    84
immler@34514
    85
  def leafs: List[MarkupNode] = {
immler@34514
    86
    if (children == Nil) return List(this)
immler@34514
    87
    else return children flatMap (_.leafs)
immler@34514
    88
  }
immler@34514
    89
immler@34514
    90
  def flatten: List[MarkupNode] = {
immler@34514
    91
    var next_x = start
immler@34514
    92
    if(children.length == 0) List(this)
immler@34514
    93
    else {
immler@34514
    94
      val filled_gaps = for {
immler@34514
    95
        child <- children
immler@34514
    96
        markups = if (next_x < child.start) {
immler@34514
    97
          new MarkupNode(base, next_x, child.start, id, kind, desc) :: child.flatten
immler@34514
    98
        } else child.flatten
immler@34514
    99
        update = (next_x = child.stop)
immler@34514
   100
        markup <- markups
immler@34514
   101
      } yield markup
immler@34514
   102
      if (next_x <= stop) filled_gaps + new MarkupNode(base, next_x, stop, id, kind, desc)
immler@34514
   103
      else filled_gaps
immler@34514
   104
    }
immler@34514
   105
  }
immler@34514
   106
immler@34401
   107
  def insert(new_child : MarkupNode) : Unit = {
wenzelm@34503
   108
    if (new_child fitting_into this) {
wenzelm@34503
   109
      for (child <- children) {
wenzelm@34503
   110
        if (new_child fitting_into child)
immler@34401
   111
          child insert new_child
immler@34401
   112
      }
wenzelm@34503
   113
      if (new_child orphan) {
immler@34401
   114
        // new_child did not fit into children of this
immler@34401
   115
        // -> insert new_child between this and its children
wenzelm@34503
   116
        for (child <- children) {
wenzelm@34503
   117
          if (child fitting_into new_child) {
immler@34401
   118
            new_child add child
immler@34400
   119
          }
immler@34400
   120
        }
immler@34401
   121
        this add new_child
immler@34401
   122
        this remove new_child.children
immler@34400
   123
      }
immler@34400
   124
    } else {
immler@34514
   125
      System.err.println("ignored nonfitting markup " + new_child.id + new_child.kind + new_child.desc
immler@34514
   126
                         + "(" +new_child.start + ", "+ new_child.stop + ")")
immler@34400
   127
    }
immler@34400
   128
  }
immler@34393
   129
immler@34401
   130
  // does this fit into node?
immler@34401
   131
  def fitting_into(node : MarkupNode) = node.start <= this.start &&
immler@34514
   132
    node.stop >= this.stop
immler@34514
   133
immler@34393
   134
}