src/Pure/PIDE/markup_node.scala
author wenzelm
Sun Aug 15 22:48:56 2010 +0200 (2010-08-15)
changeset 38426 2858ec7b6dd8
parent 38373 e8197eea3cd0
child 38478 7766812a01e7
permissions -rw-r--r--
specific types Text.Offset and Text.Range;
minor tuning;
wenzelm@36676
     1
/*  Title:      Pure/PIDE/markup_node.scala
wenzelm@36676
     2
    Author:     Fabian Immler, TU Munich
wenzelm@36676
     3
    Author:     Makarius
wenzelm@36676
     4
wenzelm@38373
     5
Text markup nodes.
wenzelm@36676
     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@38426
    15
case class Markup_Node(val range: Text.Range, val info: Any)
wenzelm@34582
    16
{
wenzelm@34717
    17
  def fits_into(that: Markup_Node): Boolean =
wenzelm@38426
    18
    that.range.start <= this.range.start && this.range.stop <= that.range.stop
wenzelm@34717
    19
}
wenzelm@34717
    20
immler@34656
    21
wenzelm@36680
    22
case class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree])
wenzelm@34717
    23
{
wenzelm@36680
    24
  private def add(branch: Markup_Tree) =   // FIXME avoid sort
wenzelm@38426
    25
    copy(branches = (branch :: branches).sortWith((a, b) => a.node.range.start < b.node.range.start))
immler@34557
    26
wenzelm@36680
    27
  private def remove(bs: List[Markup_Tree]) =
wenzelm@36680
    28
    copy(branches = branches.filterNot(bs.contains(_)))
immler@34393
    29
wenzelm@34717
    30
  def + (new_tree: Markup_Tree): Markup_Tree =
wenzelm@34703
    31
  {
wenzelm@34717
    32
    val new_node = new_tree.node
wenzelm@34717
    33
    if (new_node fits_into node) {
wenzelm@34703
    34
      var inserted = false
wenzelm@34717
    35
      val new_branches =
wenzelm@34717
    36
        branches.map(branch =>
wenzelm@34717
    37
          if ((new_node fits_into branch.node) && !inserted) {
wenzelm@34717
    38
            inserted = true
wenzelm@34717
    39
            branch + new_tree
wenzelm@34717
    40
          }
wenzelm@34717
    41
          else branch)
wenzelm@34703
    42
      if (!inserted) {
wenzelm@34717
    43
        // new_tree did not fit into children of this
wenzelm@34717
    44
        // -> insert between this and its branches
wenzelm@34717
    45
        val fitting = branches filter(_.node fits_into new_node)
wenzelm@34717
    46
        (this remove fitting) add ((new_tree /: fitting)(_ + _))
wenzelm@34703
    47
      }
wenzelm@36680
    48
      else copy(branches = new_branches)
wenzelm@34703
    49
    }
wenzelm@34703
    50
    else {
wenzelm@37189
    51
      System.err.println("Ignored nonfitting markup: " + new_node)
wenzelm@34703
    52
      this
wenzelm@34703
    53
    }
wenzelm@34703
    54
  }
wenzelm@34703
    55
wenzelm@34717
    56
  def flatten: List[Markup_Node] =
wenzelm@34717
    57
  {
wenzelm@38426
    58
    var next_x = node.range.start
wenzelm@34717
    59
    if (branches.isEmpty) List(this.node)
immler@34514
    60
    else {
wenzelm@34717
    61
      val filled_gaps =
wenzelm@34717
    62
        for {
wenzelm@34717
    63
          child <- branches
wenzelm@34717
    64
          markups =
wenzelm@38426
    65
            if (next_x < child.node.range.start)
wenzelm@38426
    66
              new Markup_Node(Text.Range(next_x, child.node.range.start), node.info) :: child.flatten
wenzelm@34717
    67
            else child.flatten
wenzelm@38426
    68
          update = (next_x = child.node.range.stop)
wenzelm@34717
    69
          markup <- markups
wenzelm@34717
    70
        } yield markup
wenzelm@38426
    71
      if (next_x < node.range.stop)
wenzelm@38426
    72
        filled_gaps ::: List(new Markup_Node(Text.Range(next_x, node.range.stop), node.info))
immler@34514
    73
      else filled_gaps
immler@34514
    74
    }
immler@34514
    75
  }
wenzelm@34717
    76
}
immler@34514
    77
wenzelm@34717
    78
wenzelm@36680
    79
case class Markup_Text(val markup: List[Markup_Tree], val content: String)
wenzelm@34717
    80
{
wenzelm@38426
    81
  private val root = new Markup_Tree(new Markup_Node(Text.Range(0, content.length), None), markup)  // FIXME !?
wenzelm@34717
    82
wenzelm@34717
    83
  def + (new_tree: Markup_Tree): Markup_Text =
wenzelm@34717
    84
    new Markup_Text((root + new_tree).branches, content)
wenzelm@34717
    85
wenzelm@34717
    86
  def filter(pred: Markup_Node => Boolean): Markup_Text =
wenzelm@34701
    87
  {
wenzelm@34717
    88
    def filt(tree: Markup_Tree): List[Markup_Tree] =
wenzelm@34717
    89
    {
wenzelm@34717
    90
      val branches = tree.branches.flatMap(filt(_))
wenzelm@36680
    91
      if (pred(tree.node)) List(tree.copy(branches = branches))
wenzelm@34717
    92
      else branches
wenzelm@34717
    93
    }
wenzelm@34717
    94
    new Markup_Text(markup.flatMap(filt(_)), content)
immler@34559
    95
  }
immler@34559
    96
wenzelm@34717
    97
  def flatten: List[Markup_Node] = markup.flatten(_.flatten)
wenzelm@34717
    98
wenzelm@34717
    99
  def swing_tree(swing_node: Markup_Node => DefaultMutableTreeNode): DefaultMutableTreeNode =
wenzelm@34717
   100
  {
wenzelm@34717
   101
    def swing(tree: Markup_Tree): DefaultMutableTreeNode =
wenzelm@34717
   102
    {
wenzelm@34717
   103
      val node = swing_node(tree.node)
wenzelm@34717
   104
      tree.branches foreach ((branch: Markup_Tree) => node.add(swing(branch)))
wenzelm@34717
   105
      node
wenzelm@34717
   106
    }
wenzelm@34717
   107
    swing(root)
wenzelm@34717
   108
  }
immler@34393
   109
}