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