src/Tools/jEdit/src/prover/MarkupNode.scala
author wenzelm
Thu Sep 03 17:48:02 2009 +0200 (2009-09-03)
changeset 34701 80b0add08eef
parent 34676 9e725d34df7b
child 34703 ff037c17332a
permissions -rw-r--r--
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
tuned;
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@34582
    52
  def dfs: List[MarkupNode] = {
immler@34401
    53
    var all = Nil : List[MarkupNode]
wenzelm@34503
    54
    for (child <- children)
immler@34401
    55
      all = child.dfs ::: all
immler@34401
    56
    all = this :: all
immler@34401
    57
    all
immler@34401
    58
  }
immler@34401
    59
wenzelm@34701
    60
  def leafs: List[MarkupNode] =
wenzelm@34701
    61
  {
immler@34514
    62
    if (children == Nil) return List(this)
immler@34514
    63
    else return children flatMap (_.leafs)
immler@34514
    64
  }
immler@34514
    65
immler@34514
    66
  def flatten: List[MarkupNode] = {
immler@34514
    67
    var next_x = start
immler@34514
    68
    if(children.length == 0) List(this)
immler@34514
    69
    else {
immler@34514
    70
      val filled_gaps = for {
immler@34514
    71
        child <- children
wenzelm@34582
    72
        markups =
wenzelm@34582
    73
          if (next_x < child.start) {
wenzelm@34582
    74
            new MarkupNode(base, next_x, child.start, Nil, id, content, info) :: child.flatten
wenzelm@34582
    75
          } else child.flatten
immler@34514
    76
        update = (next_x = child.stop)
immler@34514
    77
        markup <- markups
immler@34514
    78
      } yield markup
wenzelm@34582
    79
      if (next_x < stop)
wenzelm@34582
    80
        filled_gaps + new MarkupNode(base, next_x, stop, Nil, id, content, info)
immler@34514
    81
      else filled_gaps
immler@34514
    82
    }
immler@34514
    83
  }
immler@34514
    84
wenzelm@34701
    85
  def filter(p: MarkupNode => Boolean): List[MarkupNode] =
wenzelm@34701
    86
  {
immler@34559
    87
    val filtered = children.flatMap(_.filter(p))
immler@34559
    88
    if (p(this)) List(this set_children(filtered))
immler@34559
    89
    else filtered
immler@34559
    90
  }
immler@34559
    91
wenzelm@34701
    92
  def + (new_child: MarkupNode): MarkupNode =
wenzelm@34701
    93
  {
wenzelm@34503
    94
    if (new_child fitting_into this) {
immler@34561
    95
      var inserted = false
wenzelm@34582
    96
      val new_children =
wenzelm@34582
    97
        children.map(c =>
wenzelm@34582
    98
          if ((new_child fitting_into c) && !inserted) {inserted = true; c + new_child}
wenzelm@34582
    99
          else c)
immler@34561
   100
      if (!inserted) {
wenzelm@34582
   101
        // new_child did not fit into children of this
wenzelm@34582
   102
        // -> insert new_child between this and its children
immler@34561
   103
        val fitting = children filter(_ fitting_into new_child)
immler@34561
   104
        (this remove fitting) add ((new_child /: fitting) (_ + _))
immler@34401
   105
      }
immler@34557
   106
      else this set_children new_children
wenzelm@34701
   107
    }
wenzelm@34701
   108
    else {
immler@34590
   109
      System.err.println("ignored nonfitting markup: " + new_child)
immler@34590
   110
      this
immler@34400
   111
    }
immler@34400
   112
  }
immler@34393
   113
immler@34401
   114
  // does this fit into node?
wenzelm@34582
   115
  def fitting_into(node: MarkupNode) = node.start <= this.start && node.stop >= this.stop
immler@34514
   116
wenzelm@34582
   117
  override def toString =
wenzelm@34582
   118
    "([" + start + " - " + stop + "] " + id + "( " + content + "): " + info.toString
immler@34393
   119
}