src/Tools/jEdit/src/prover/MarkupNode.scala
author immler@in.tum.de
Wed, 22 Apr 2009 17:35:49 +0200
changeset 34554 7dc6c231da40
parent 34517 163cda249619
child 34555 7c001369956a
permissions -rw-r--r--
abs. stops, markup nodes depend on doc-version; fixed missing positions in ProofDocument.text_changed; relink only changed commands in ProofDocument.token_changed
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
     1
/*
34407
aad6834ba380 added some headers and comments;
wenzelm
parents: 34402
diff changeset
     2
 * Document markup nodes, with connection to Swing tree model
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
     3
 *
34407
aad6834ba380 added some headers and comments;
wenzelm
parents: 34402
diff changeset
     4
 * @author Fabian Immler, TU Munich
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
     5
 */
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
     6
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
     7
package isabelle.prover
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
     8
34554
7dc6c231da40 abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents: 34517
diff changeset
     9
import isabelle.proofdocument.ProofDocument
7dc6c231da40 abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents: 34517
diff changeset
    10
34400
1b61a92f8675 MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents: 34393
diff changeset
    11
import sidekick.IAsset
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
    12
import javax.swing._
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
    13
import javax.swing.text.Position
34400
1b61a92f8675 MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents: 34393
diff changeset
    14
import javax.swing.tree._
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
    15
34401
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    16
object MarkupNode {
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    17
34554
7dc6c231da40 abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents: 34517
diff changeset
    18
  def markup2default_node(node: MarkupNode, cmd: Command, doc: ProofDocument) : DefaultMutableTreeNode = {
34401
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    19
34480
017fae24829f simplified implicit convertion Int => Position;
wenzelm
parents: 34407
diff changeset
    20
    implicit def int2pos(offset: Int): Position =
34554
7dc6c231da40 abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents: 34517
diff changeset
    21
      new Position { def getOffset = offset; override def toString = offset.toString}
34401
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    22
34480
017fae24829f simplified implicit convertion Int => Position;
wenzelm
parents: 34407
diff changeset
    23
    object RelativeAsset extends IAsset {
34401
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    24
      override def getIcon : Icon = null
34514
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
    25
      override def getShortString : String = node.kind
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
    26
      override def getLongString : String = node.desc
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
    27
      override def getName : String = node.id
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
    28
      override def setName (name : String) = ()
34401
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    29
      override def setStart(start : Position) = ()
34554
7dc6c231da40 abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents: 34517
diff changeset
    30
      override def getStart : Position = node.abs_start(doc)
34401
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    31
      override def setEnd(end : Position) = ()
34554
7dc6c231da40 abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents: 34517
diff changeset
    32
      override def getEnd : Position = node.abs_stop(doc)
7dc6c231da40 abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents: 34517
diff changeset
    33
      override def toString = node.id + ": " + node.kind + "[" + getStart + " - " + getEnd + "]"
34401
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    34
    }
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
    35
34401
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    36
    new DefaultMutableTreeNode(RelativeAsset)
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    37
  }
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    38
}
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    39
34514
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
    40
class MarkupNode (val base : Command, val start : Int, val stop : Int,
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
    41
                    val id : String, val kind : String, val desc : String) {
34401
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    42
34554
7dc6c231da40 abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents: 34517
diff changeset
    43
  def swing_node(doc: ProofDocument) : DefaultMutableTreeNode = {
7dc6c231da40 abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents: 34517
diff changeset
    44
    val node = MarkupNode.markup2default_node (this, base, doc)
7dc6c231da40 abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents: 34517
diff changeset
    45
    for (c <- children) node add c.swing_node(doc)
7dc6c231da40 abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents: 34517
diff changeset
    46
    node
7dc6c231da40 abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents: 34517
diff changeset
    47
  }
7dc6c231da40 abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents: 34517
diff changeset
    48
    
7dc6c231da40 abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents: 34517
diff changeset
    49
  def abs_start(doc: ProofDocument) = base.start(doc) + start
7dc6c231da40 abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents: 34517
diff changeset
    50
  def abs_stop(doc: ProofDocument) = base.start(doc) + stop
34401
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    51
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    52
  var parent : MarkupNode = null
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    53
  def orphan = parent == null
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    54
34554
7dc6c231da40 abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents: 34517
diff changeset
    55
  var children : List[MarkupNode] = Nil
34514
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
    56
34401
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    57
  private def add(child : MarkupNode) {
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    58
    child parent = this
34554
7dc6c231da40 abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents: 34517
diff changeset
    59
    children = (child :: children) sort ((a, b) => a.start < b.start)
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
    60
  }
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
    61
34401
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    62
  private def remove(nodes : List[MarkupNode]) {
34554
7dc6c231da40 abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents: 34517
diff changeset
    63
    children = children diff nodes
34401
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    64
  }
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
    65
34401
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    66
  def dfs : List[MarkupNode] = {
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    67
    var all = Nil : List[MarkupNode]
34503
7d0726f19d04 tuned whitespace;
wenzelm
parents: 34480
diff changeset
    68
    for (child <- children)
34401
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    69
      all = child.dfs ::: all
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    70
    all = this :: all
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    71
    all
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    72
  }
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    73
34514
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
    74
  def leafs: List[MarkupNode] = {
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
    75
    if (children == Nil) return List(this)
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
    76
    else return children flatMap (_.leafs)
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
    77
  }
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
    78
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
    79
  def flatten: List[MarkupNode] = {
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
    80
    var next_x = start
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
    81
    if(children.length == 0) List(this)
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
    82
    else {
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
    83
      val filled_gaps = for {
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
    84
        child <- children
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
    85
        markups = if (next_x < child.start) {
34517
163cda249619 implemented markTokens;
immler@in.tum.de
parents: 34514
diff changeset
    86
          new MarkupNode(base, next_x, child.start, id, kind, "") :: child.flatten
34514
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
    87
        } else child.flatten
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
    88
        update = (next_x = child.stop)
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
    89
        markup <- markups
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
    90
      } yield markup
34517
163cda249619 implemented markTokens;
immler@in.tum.de
parents: 34514
diff changeset
    91
      if (next_x < stop) filled_gaps + new MarkupNode(base, next_x, stop, id, kind, "")
34514
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
    92
      else filled_gaps
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
    93
    }
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
    94
  }
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
    95
34401
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    96
  def insert(new_child : MarkupNode) : Unit = {
34503
7d0726f19d04 tuned whitespace;
wenzelm
parents: 34480
diff changeset
    97
    if (new_child fitting_into this) {
7d0726f19d04 tuned whitespace;
wenzelm
parents: 34480
diff changeset
    98
      for (child <- children) {
7d0726f19d04 tuned whitespace;
wenzelm
parents: 34480
diff changeset
    99
        if (new_child fitting_into child)
34401
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
   100
          child insert new_child
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
   101
      }
34503
7d0726f19d04 tuned whitespace;
wenzelm
parents: 34480
diff changeset
   102
      if (new_child orphan) {
34401
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
   103
        // new_child did not fit into children of this
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
   104
        // -> insert new_child between this and its children
34503
7d0726f19d04 tuned whitespace;
wenzelm
parents: 34480
diff changeset
   105
        for (child <- children) {
7d0726f19d04 tuned whitespace;
wenzelm
parents: 34480
diff changeset
   106
          if (child fitting_into new_child) {
34401
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
   107
            new_child add child
34400
1b61a92f8675 MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents: 34393
diff changeset
   108
          }
1b61a92f8675 MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents: 34393
diff changeset
   109
        }
34401
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
   110
        this add new_child
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
   111
        this remove new_child.children
34400
1b61a92f8675 MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents: 34393
diff changeset
   112
      }
1b61a92f8675 MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents: 34393
diff changeset
   113
    } else {
34514
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
   114
      System.err.println("ignored nonfitting markup " + new_child.id + new_child.kind + new_child.desc
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
   115
                         + "(" +new_child.start + ", "+ new_child.stop + ")")
34400
1b61a92f8675 MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents: 34393
diff changeset
   116
    }
1b61a92f8675 MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents: 34393
diff changeset
   117
  }
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
   118
34401
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
   119
  // does this fit into node?
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
   120
  def fitting_into(node : MarkupNode) = node.start <= this.start &&
34514
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
   121
    node.stop >= this.stop
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
   122
34517
163cda249619 implemented markTokens;
immler@in.tum.de
parents: 34514
diff changeset
   123
  override def toString = "([" + start + " - " + stop + "] " + id + "( " + kind + "): " + desc
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
   124
}