src/Pure/Thy/markup_node.scala
author wenzelm
Mon Jan 11 23:00:05 2010 +0100 (2010-01-11)
changeset 34871 e596a0b71f3c
parent 34760 src/Tools/jEdit/src/proofdocument/markup_node.scala@dc7f5e0d9d27
child 36011 3ff725ac13a4
permissions -rw-r--r--
incorporate "proofdocument" part into main Isabelle/Pure.jar -- except for html_panel.scala, which depends on external library (Lobo/Cobra browser);
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
wenzelm@34760
     5
 * @author Makarius
immler@34393
     6
 */
immler@34393
     7
wenzelm@34871
     8
package isabelle
immler@34393
     9
wenzelm@34701
    10
wenzelm@34701
    11
import javax.swing.tree.DefaultMutableTreeNode
wenzelm@34701
    12
immler@34554
    13
immler@34393
    14
wenzelm@34717
    15
class Markup_Node(val start: Int, val stop: Int, val info: Any)
wenzelm@34582
    16
{
wenzelm@34717
    17
  def fits_into(that: Markup_Node): Boolean =
wenzelm@34717
    18
    that.start <= this.start && this.stop <= that.stop
wenzelm@34717
    19
}
wenzelm@34717
    20
immler@34656
    21
wenzelm@34717
    22
class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree])
wenzelm@34717
    23
{
wenzelm@34717
    24
  def set_branches(bs: List[Markup_Tree]): Markup_Tree = new Markup_Tree(node, bs)
immler@34557
    25
wenzelm@34717
    26
  private def add(branch: Markup_Tree) =   // FIXME avoid sort
wenzelm@34717
    27
    set_branches((branch :: branches) sort ((a, b) => a.node.start < b.node.start))
immler@34514
    28
wenzelm@34717
    29
  private def remove(bs: List[Markup_Tree]) = set_branches(branches -- bs)
immler@34393
    30
wenzelm@34717
    31
  def + (new_tree: Markup_Tree): Markup_Tree =
wenzelm@34703
    32
  {
wenzelm@34717
    33
    val new_node = new_tree.node
wenzelm@34717
    34
    if (new_node fits_into node) {
wenzelm@34703
    35
      var inserted = false
wenzelm@34717
    36
      val new_branches =
wenzelm@34717
    37
        branches.map(branch =>
wenzelm@34717
    38
          if ((new_node fits_into branch.node) && !inserted) {
wenzelm@34717
    39
            inserted = true
wenzelm@34717
    40
            branch + new_tree
wenzelm@34717
    41
          }
wenzelm@34717
    42
          else branch)
wenzelm@34703
    43
      if (!inserted) {
wenzelm@34717
    44
        // new_tree did not fit into children of this
wenzelm@34717
    45
        // -> insert between this and its branches
wenzelm@34717
    46
        val fitting = branches filter(_.node fits_into new_node)
wenzelm@34717
    47
        (this remove fitting) add ((new_tree /: fitting)(_ + _))
wenzelm@34703
    48
      }
wenzelm@34717
    49
      else set_branches(new_branches)
wenzelm@34703
    50
    }
wenzelm@34703
    51
    else {
wenzelm@34717
    52
      System.err.println("ignored nonfitting markup: " + new_node)
wenzelm@34703
    53
      this
wenzelm@34703
    54
    }
wenzelm@34703
    55
  }
wenzelm@34703
    56
wenzelm@34717
    57
  def flatten: List[Markup_Node] =
wenzelm@34717
    58
  {
wenzelm@34717
    59
    var next_x = node.start
wenzelm@34717
    60
    if (branches.isEmpty) List(this.node)
immler@34514
    61
    else {
wenzelm@34717
    62
      val filled_gaps =
wenzelm@34717
    63
        for {
wenzelm@34717
    64
          child <- branches
wenzelm@34717
    65
          markups =
wenzelm@34717
    66
            if (next_x < child.node.start)
wenzelm@34717
    67
              new Markup_Node(next_x, child.node.start, node.info) :: child.flatten
wenzelm@34717
    68
            else child.flatten
wenzelm@34717
    69
          update = (next_x = child.node.stop)
wenzelm@34717
    70
          markup <- markups
wenzelm@34717
    71
        } yield markup
wenzelm@34717
    72
      if (next_x < node.stop)
wenzelm@34717
    73
        filled_gaps + new Markup_Node(next_x, node.stop, node.info)
immler@34514
    74
      else filled_gaps
immler@34514
    75
    }
immler@34514
    76
  }
wenzelm@34717
    77
}
immler@34514
    78
wenzelm@34717
    79
wenzelm@34717
    80
class Markup_Text(val markup: List[Markup_Tree], val content: String)
wenzelm@34717
    81
{
wenzelm@34717
    82
  private lazy val root =
wenzelm@34717
    83
    new Markup_Tree(new Markup_Node(0, content.length, None), markup)
wenzelm@34717
    84
wenzelm@34717
    85
  def + (new_tree: Markup_Tree): Markup_Text =
wenzelm@34717
    86
    new Markup_Text((root + new_tree).branches, content)
wenzelm@34717
    87
wenzelm@34717
    88
  def filter(pred: Markup_Node => Boolean): Markup_Text =
wenzelm@34701
    89
  {
wenzelm@34717
    90
    def filt(tree: Markup_Tree): List[Markup_Tree] =
wenzelm@34717
    91
    {
wenzelm@34717
    92
      val branches = tree.branches.flatMap(filt(_))
wenzelm@34717
    93
      if (pred(tree.node)) List(tree.set_branches(branches))
wenzelm@34717
    94
      else branches
wenzelm@34717
    95
    }
wenzelm@34717
    96
    new Markup_Text(markup.flatMap(filt(_)), content)
immler@34559
    97
  }
immler@34559
    98
wenzelm@34717
    99
  def flatten: List[Markup_Node] = markup.flatten(_.flatten)
wenzelm@34717
   100
wenzelm@34717
   101
  def swing_tree(swing_node: Markup_Node => DefaultMutableTreeNode): DefaultMutableTreeNode =
wenzelm@34717
   102
  {
wenzelm@34717
   103
    def swing(tree: Markup_Tree): DefaultMutableTreeNode =
wenzelm@34717
   104
    {
wenzelm@34717
   105
      val node = swing_node(tree.node)
wenzelm@34717
   106
      tree.branches foreach ((branch: Markup_Tree) => node.add(swing(branch)))
wenzelm@34717
   107
      node
wenzelm@34717
   108
    }
wenzelm@34717
   109
    swing(root)
wenzelm@34717
   110
  }
immler@34393
   111
}