src/Tools/jEdit/src/prover/MarkupNode.scala
author immler@in.tum.de
Fri May 22 13:43:34 2009 +0200 (2009-05-22)
changeset 34559 2adb23c3e5d1
parent 34558 668fae39d86d
child 34560 08f0d81c6833
permissions -rw-r--r--
implemented filter on markup-tree
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@34554
     9
import isabelle.proofdocument.ProofDocument
immler@34554
    10
immler@34400
    11
import sidekick.IAsset
immler@34393
    12
import javax.swing._
immler@34393
    13
import javax.swing.text.Position
immler@34400
    14
import javax.swing.tree._
immler@34393
    15
immler@34401
    16
object MarkupNode {
immler@34401
    17
immler@34554
    18
  def markup2default_node(node: MarkupNode, cmd: Command, doc: ProofDocument) : DefaultMutableTreeNode = {
immler@34401
    19
wenzelm@34480
    20
    implicit def int2pos(offset: Int): Position =
immler@34554
    21
      new Position { def getOffset = offset; override def toString = offset.toString}
immler@34401
    22
wenzelm@34480
    23
    object RelativeAsset extends IAsset {
immler@34401
    24
      override def getIcon : Icon = null
immler@34555
    25
      override def getShortString : String = node.content
immler@34514
    26
      override def getLongString : String = node.desc
immler@34514
    27
      override def getName : String = node.id
immler@34514
    28
      override def setName (name : String) = ()
immler@34401
    29
      override def setStart(start : Position) = ()
immler@34554
    30
      override def getStart : Position = node.abs_start(doc)
immler@34401
    31
      override def setEnd(end : Position) = ()
immler@34554
    32
      override def getEnd : Position = node.abs_stop(doc)
immler@34555
    33
      override def toString = node.id + ": " + node.content + "[" + getStart + " - " + getEnd + "]"
immler@34401
    34
    }
immler@34393
    35
immler@34401
    36
    new DefaultMutableTreeNode(RelativeAsset)
immler@34401
    37
  }
immler@34401
    38
}
immler@34401
    39
immler@34514
    40
class MarkupNode (val base : Command, val start : Int, val stop : Int,
immler@34557
    41
                  val children: List[MarkupNode],
immler@34557
    42
                  val id : String, val content : String, val desc : String) {
immler@34401
    43
immler@34554
    44
  def swing_node(doc: ProofDocument) : DefaultMutableTreeNode = {
immler@34554
    45
    val node = MarkupNode.markup2default_node (this, base, doc)
immler@34557
    46
    children.map(node add _.swing_node(doc))
immler@34554
    47
    node
immler@34554
    48
  }
immler@34557
    49
immler@34554
    50
  def abs_start(doc: ProofDocument) = base.start(doc) + start
immler@34554
    51
  def abs_stop(doc: ProofDocument) = base.start(doc) + stop
immler@34401
    52
immler@34557
    53
  def set_children(newchildren: List[MarkupNode]): MarkupNode =
immler@34557
    54
    new MarkupNode(base, start, stop, newchildren, id, content, desc)
immler@34514
    55
immler@34557
    56
  def add(child : MarkupNode) = set_children ((child :: children) sort ((a, b) => a.start < b.start))
immler@34393
    57
immler@34557
    58
  def remove(nodes : List[MarkupNode]) = set_children(children diff nodes)
immler@34393
    59
immler@34401
    60
  def dfs : List[MarkupNode] = {
immler@34401
    61
    var all = Nil : List[MarkupNode]
wenzelm@34503
    62
    for (child <- children)
immler@34401
    63
      all = child.dfs ::: all
immler@34401
    64
    all = this :: all
immler@34401
    65
    all
immler@34401
    66
  }
immler@34401
    67
immler@34514
    68
  def leafs: List[MarkupNode] = {
immler@34514
    69
    if (children == Nil) return List(this)
immler@34514
    70
    else return children flatMap (_.leafs)
immler@34514
    71
  }
immler@34514
    72
immler@34514
    73
  def flatten: List[MarkupNode] = {
immler@34514
    74
    var next_x = start
immler@34514
    75
    if(children.length == 0) List(this)
immler@34514
    76
    else {
immler@34514
    77
      val filled_gaps = for {
immler@34514
    78
        child <- children
immler@34514
    79
        markups = if (next_x < child.start) {
immler@34558
    80
          new MarkupNode(base, next_x, child.start, Nil, id, content, desc) :: child.flatten
immler@34514
    81
        } else child.flatten
immler@34514
    82
        update = (next_x = child.stop)
immler@34514
    83
        markup <- markups
immler@34514
    84
      } yield markup
immler@34558
    85
      if (next_x < stop) filled_gaps + new MarkupNode(base, next_x, stop, Nil, id, content, desc)
immler@34514
    86
      else filled_gaps
immler@34514
    87
    }
immler@34514
    88
  }
immler@34514
    89
immler@34559
    90
  def filter(p: (MarkupNode => Boolean)): List[MarkupNode] = {
immler@34559
    91
    val filtered = children.flatMap(_.filter(p))
immler@34559
    92
    if (p(this)) List(this set_children(filtered))
immler@34559
    93
    else filtered
immler@34559
    94
  }
immler@34559
    95
immler@34557
    96
  def +(new_child : MarkupNode) : MarkupNode = {
wenzelm@34503
    97
    if (new_child fitting_into this) {
immler@34557
    98
      val new_children = children.map(c => if((new_child fitting_into c)) c + new_child else c)
immler@34557
    99
      if (new_children == children) {
immler@34557
   100
        // new_child did not fit into children of this -> insert new_child between this and its children
immler@34557
   101
        val (fitting, nonfitting) = children span(_ fitting_into new_child)
immler@34557
   102
        this remove fitting add ((new_child /: fitting) (_ add _))
immler@34401
   103
      }
immler@34557
   104
      else this set_children new_children
immler@34400
   105
    } else {
immler@34557
   106
      error("ignored nonfitting markup " + new_child.id + new_child.content + new_child.desc
immler@34514
   107
                         + "(" +new_child.start + ", "+ new_child.stop + ")")
immler@34400
   108
    }
immler@34400
   109
  }
immler@34393
   110
immler@34401
   111
  // does this fit into node?
immler@34557
   112
  def fitting_into(node : MarkupNode) = node.start <= this.start && node.stop >= this.stop
immler@34514
   113
immler@34555
   114
  override def toString = "([" + start + " - " + stop + "] " + id + "( " + content + "): " + desc
immler@34393
   115
}