src/Tools/jEdit/src/prover/MarkupNode.scala
author wenzelm
Fri Sep 04 23:04:20 2009 +0200 (2009-09-04)
changeset 34703 ff037c17332a
parent 34701 80b0add08eef
child 34704 504cab625d3e
permissions -rw-r--r--
minor tuning;
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
wenzelm@34701
     9
wenzelm@34701
    10
import javax.swing.tree.DefaultMutableTreeNode
wenzelm@34701
    11
immler@34554
    12
import isabelle.proofdocument.ProofDocument
immler@34554
    13
immler@34393
    14
immler@34564
    15
abstract class MarkupInfo
immler@34577
    16
case class RootInfo() extends MarkupInfo
wenzelm@34582
    17
case class HighlightInfo(highlight: String) extends
wenzelm@34582
    18
  MarkupInfo { override def toString = highlight }
wenzelm@34582
    19
case class TypeInfo(type_kind: String) extends
wenzelm@34582
    20
  MarkupInfo { override def toString = type_kind }
immler@34568
    21
case class RefInfo(file: Option[String], line: Option[Int],
wenzelm@34582
    22
  command_id: Option[String], offset: Option[Int]) extends MarkupInfo {
wenzelm@34582
    23
    override def toString = (file, line, command_id, offset).toString
wenzelm@34582
    24
  }
immler@34564
    25
immler@34401
    26
wenzelm@34582
    27
class MarkupNode(val base: Command, val start: Int, val stop: Int,
wenzelm@34582
    28
  val children: List[MarkupNode],
wenzelm@34582
    29
  val id: String, val content: String, val info: MarkupInfo)
wenzelm@34582
    30
{
immler@34656
    31
wenzelm@34701
    32
  def swing_tree(doc: ProofDocument)
wenzelm@34701
    33
    (make_node: (MarkupNode, Command, ProofDocument) => DefaultMutableTreeNode):
wenzelm@34701
    34
      DefaultMutableTreeNode =
wenzelm@34701
    35
  {
wenzelm@34701
    36
    val node = make_node(this, base, doc)
wenzelm@34701
    37
    children.foreach(node add _.swing_tree(doc)(make_node))
immler@34554
    38
    node
immler@34554
    39
  }
immler@34557
    40
immler@34554
    41
  def abs_start(doc: ProofDocument) = base.start(doc) + start
immler@34554
    42
  def abs_stop(doc: ProofDocument) = base.start(doc) + stop
immler@34401
    43
wenzelm@34701
    44
  def set_children(new_children: List[MarkupNode]): MarkupNode =
wenzelm@34701
    45
    new MarkupNode(base, start, stop, new_children, id, content, info)
immler@34514
    46
wenzelm@34701
    47
  private def add(child: MarkupNode) =   // FIXME avoid sort?
wenzelm@34582
    48
    set_children ((child :: children) sort ((a, b) => a.start < b.start))
immler@34393
    49
wenzelm@34582
    50
  def remove(nodes: List[MarkupNode]) = set_children(children diff nodes)
immler@34393
    51
wenzelm@34703
    52
  def fits_into(node: MarkupNode): Boolean =
wenzelm@34703
    53
    node.start <= this.start && this.stop <= node.stop
wenzelm@34703
    54
wenzelm@34703
    55
  def + (new_child: MarkupNode): MarkupNode =
wenzelm@34703
    56
  {
wenzelm@34703
    57
    if (new_child fits_into this) {
wenzelm@34703
    58
      var inserted = false
wenzelm@34703
    59
      val new_children =
wenzelm@34703
    60
        children.map(c =>
wenzelm@34703
    61
          if ((new_child fits_into c) && !inserted) {inserted = true; c + new_child}
wenzelm@34703
    62
          else c)
wenzelm@34703
    63
      if (!inserted) {
wenzelm@34703
    64
        // new_child did not fit into children of this
wenzelm@34703
    65
        // -> insert new_child between this and its children
wenzelm@34703
    66
        val fitting = children filter(_ fits_into new_child)
wenzelm@34703
    67
        (this remove fitting) add ((new_child /: fitting) (_ + _))
wenzelm@34703
    68
      }
wenzelm@34703
    69
      else this set_children new_children
wenzelm@34703
    70
    }
wenzelm@34703
    71
    else {
wenzelm@34703
    72
      System.err.println("ignored nonfitting markup: " + new_child)
wenzelm@34703
    73
      this
wenzelm@34703
    74
    }
wenzelm@34703
    75
  }
wenzelm@34703
    76
wenzelm@34582
    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
wenzelm@34701
    85
  def leafs: List[MarkupNode] =
wenzelm@34701
    86
  {
wenzelm@34703
    87
    if (children.isEmpty) return List(this)
immler@34514
    88
    else return children flatMap (_.leafs)
immler@34514
    89
  }
immler@34514
    90
immler@34514
    91
  def flatten: List[MarkupNode] = {
immler@34514
    92
    var next_x = start
wenzelm@34703
    93
    if (children.isEmpty) List(this)
immler@34514
    94
    else {
immler@34514
    95
      val filled_gaps = for {
immler@34514
    96
        child <- children
wenzelm@34582
    97
        markups =
wenzelm@34582
    98
          if (next_x < child.start) {
wenzelm@34582
    99
            new MarkupNode(base, next_x, child.start, Nil, id, content, info) :: child.flatten
wenzelm@34582
   100
          } else child.flatten
immler@34514
   101
        update = (next_x = child.stop)
immler@34514
   102
        markup <- markups
immler@34514
   103
      } yield markup
wenzelm@34582
   104
      if (next_x < stop)
wenzelm@34582
   105
        filled_gaps + new MarkupNode(base, next_x, stop, Nil, id, content, info)
immler@34514
   106
      else filled_gaps
immler@34514
   107
    }
immler@34514
   108
  }
immler@34514
   109
wenzelm@34701
   110
  def filter(p: MarkupNode => Boolean): List[MarkupNode] =
wenzelm@34701
   111
  {
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
  override def toString =
wenzelm@34582
   118
    "([" + start + " - " + stop + "] " + id + "( " + content + "): " + info.toString
immler@34393
   119
}