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