src/Tools/jEdit/src/prover/MarkupNode.scala
author immler@in.tum.de
Wed Jul 15 13:49:21 2009 +0200 (2009-07-15)
changeset 34656 2740439a86b4
parent 34597 a0c84b0edb9a
child 34659 e888d0cdda9c
permissions -rw-r--r--
decode offsets with respect to symbols
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@34564
    16
abstract class MarkupInfo
immler@34577
    17
case class RootInfo() extends MarkupInfo
wenzelm@34582
    18
case class OuterInfo(highlight: String) extends
wenzelm@34582
    19
  MarkupInfo { override def toString = highlight }
wenzelm@34582
    20
case class HighlightInfo(highlight: String) extends
wenzelm@34582
    21
  MarkupInfo { override def toString = highlight }
wenzelm@34582
    22
case class TypeInfo(type_kind: String) extends
wenzelm@34582
    23
  MarkupInfo { override def toString = type_kind }
immler@34568
    24
case class RefInfo(file: Option[String], line: Option[Int],
wenzelm@34582
    25
  command_id: Option[String], offset: Option[Int]) extends MarkupInfo {
wenzelm@34582
    26
    override def toString = (file, line, command_id, offset).toString
wenzelm@34582
    27
  }
immler@34564
    28
immler@34401
    29
object MarkupNode {
immler@34401
    30
wenzelm@34582
    31
  def markup2default_node(node: MarkupNode, cmd: Command, doc: ProofDocument)
wenzelm@34582
    32
      : DefaultMutableTreeNode = {
immler@34401
    33
wenzelm@34480
    34
    implicit def int2pos(offset: Int): Position =
wenzelm@34582
    35
      new Position { def getOffset = offset; override def toString = offset.toString }
immler@34401
    36
wenzelm@34480
    37
    object RelativeAsset extends IAsset {
wenzelm@34582
    38
      override def getIcon: Icon = null
wenzelm@34582
    39
      override def getShortString: String = node.content
wenzelm@34582
    40
      override def getLongString: String = node.info.toString
wenzelm@34582
    41
      override def getName: String = node.id
wenzelm@34582
    42
      override def setName(name: String) = ()
wenzelm@34582
    43
      override def setStart(start: Position) = ()
wenzelm@34582
    44
      override def getStart: Position = node.abs_start(doc)
wenzelm@34582
    45
      override def setEnd(end: Position) = ()
wenzelm@34582
    46
      override def getEnd: Position = node.abs_stop(doc)
immler@34555
    47
      override def toString = node.id + ": " + node.content + "[" + getStart + " - " + getEnd + "]"
immler@34401
    48
    }
immler@34393
    49
immler@34401
    50
    new DefaultMutableTreeNode(RelativeAsset)
immler@34401
    51
  }
immler@34401
    52
}
immler@34401
    53
wenzelm@34582
    54
class MarkupNode(val base: Command, val start: Int, val stop: Int,
wenzelm@34582
    55
  val children: List[MarkupNode],
wenzelm@34582
    56
  val id: String, val content: String, val info: MarkupInfo)
wenzelm@34582
    57
{
immler@34656
    58
immler@34656
    59
  def transform(f: Int => Int): MarkupNode = new MarkupNode(base,
immler@34656
    60
    f(start), f(stop), children map (_ transform f), id, content, info)
immler@34656
    61
wenzelm@34582
    62
  def swing_node(doc: ProofDocument): DefaultMutableTreeNode = {
immler@34554
    63
    val node = MarkupNode.markup2default_node (this, base, doc)
immler@34557
    64
    children.map(node add _.swing_node(doc))
immler@34554
    65
    node
immler@34554
    66
  }
immler@34557
    67
immler@34554
    68
  def abs_start(doc: ProofDocument) = base.start(doc) + start
immler@34554
    69
  def abs_stop(doc: ProofDocument) = base.start(doc) + stop
immler@34401
    70
immler@34557
    71
  def set_children(newchildren: List[MarkupNode]): MarkupNode =
immler@34564
    72
    new MarkupNode(base, start, stop, newchildren, id, content, info)
immler@34514
    73
wenzelm@34582
    74
  def add(child: MarkupNode) =
wenzelm@34582
    75
    set_children ((child :: children) sort ((a, b) => a.start < b.start))
immler@34393
    76
wenzelm@34582
    77
  def remove(nodes: List[MarkupNode]) = set_children(children diff nodes)
immler@34393
    78
wenzelm@34582
    79
  def dfs: List[MarkupNode] = {
immler@34401
    80
    var all = Nil : List[MarkupNode]
wenzelm@34503
    81
    for (child <- children)
immler@34401
    82
      all = child.dfs ::: all
immler@34401
    83
    all = this :: all
immler@34401
    84
    all
immler@34401
    85
  }
immler@34401
    86
immler@34514
    87
  def leafs: List[MarkupNode] = {
immler@34514
    88
    if (children == Nil) return List(this)
immler@34514
    89
    else return children flatMap (_.leafs)
immler@34514
    90
  }
immler@34514
    91
immler@34514
    92
  def flatten: List[MarkupNode] = {
immler@34514
    93
    var next_x = start
immler@34514
    94
    if(children.length == 0) List(this)
immler@34514
    95
    else {
immler@34514
    96
      val filled_gaps = for {
immler@34514
    97
        child <- children
wenzelm@34582
    98
        markups =
wenzelm@34582
    99
          if (next_x < child.start) {
wenzelm@34582
   100
            new MarkupNode(base, next_x, child.start, Nil, id, content, info) :: child.flatten
wenzelm@34582
   101
          } else child.flatten
immler@34514
   102
        update = (next_x = child.stop)
immler@34514
   103
        markup <- markups
immler@34514
   104
      } yield markup
wenzelm@34582
   105
      if (next_x < stop)
wenzelm@34582
   106
        filled_gaps + new MarkupNode(base, next_x, stop, Nil, id, content, info)
immler@34514
   107
      else filled_gaps
immler@34514
   108
    }
immler@34514
   109
  }
immler@34514
   110
wenzelm@34582
   111
  def filter(p: MarkupNode => Boolean): List[MarkupNode] = {
immler@34559
   112
    val filtered = children.flatMap(_.filter(p))
immler@34559
   113
    if (p(this)) List(this set_children(filtered))
immler@34559
   114
    else filtered
immler@34559
   115
  }
immler@34559
   116
wenzelm@34582
   117
  def +(new_child: MarkupNode): MarkupNode = {
wenzelm@34503
   118
    if (new_child fitting_into this) {
immler@34561
   119
      var inserted = false
wenzelm@34582
   120
      val new_children =
wenzelm@34582
   121
        children.map(c =>
wenzelm@34582
   122
          if ((new_child fitting_into c) && !inserted) {inserted = true; c + new_child}
wenzelm@34582
   123
          else c)
immler@34561
   124
      if (!inserted) {
wenzelm@34582
   125
        // new_child did not fit into children of this
wenzelm@34582
   126
        // -> insert new_child between this and its children
immler@34561
   127
        val fitting = children filter(_ fitting_into new_child)
immler@34561
   128
        (this remove fitting) add ((new_child /: fitting) (_ + _))
immler@34401
   129
      }
immler@34557
   130
      else this set_children new_children
immler@34400
   131
    } else {
immler@34590
   132
      System.err.println("ignored nonfitting markup: " + new_child)
immler@34590
   133
      this
immler@34400
   134
    }
immler@34400
   135
  }
immler@34393
   136
immler@34401
   137
  // does this fit into node?
wenzelm@34582
   138
  def fitting_into(node: MarkupNode) = node.start <= this.start && node.stop >= this.stop
immler@34514
   139
wenzelm@34582
   140
  override def toString =
wenzelm@34582
   141
    "([" + start + " - " + stop + "] " + id + "( " + content + "): " + info.toString
immler@34393
   142
}