src/Tools/jEdit/src/proofdocument/markup_node.scala
changeset 34759 bfea7839d9e1
parent 34717 3f32e08bbb6c
child 34760 dc7f5e0d9d27
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/jEdit/src/proofdocument/markup_node.scala	Tue Dec 08 14:49:01 2009 +0100
     1.3 @@ -0,0 +1,111 @@
     1.4 +/*
     1.5 + * Document markup nodes, with connection to Swing tree model
     1.6 + *
     1.7 + * @author Fabian Immler, TU Munich
     1.8 + */
     1.9 +
    1.10 +package isabelle.prover
    1.11 +
    1.12 +
    1.13 +import javax.swing.tree.DefaultMutableTreeNode
    1.14 +
    1.15 +import isabelle.proofdocument.ProofDocument
    1.16 +
    1.17 +
    1.18 +class Markup_Node(val start: Int, val stop: Int, val info: Any)
    1.19 +{
    1.20 +  def fits_into(that: Markup_Node): Boolean =
    1.21 +    that.start <= this.start && this.stop <= that.stop
    1.22 +}
    1.23 +
    1.24 +
    1.25 +class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree])
    1.26 +{
    1.27 +  def set_branches(bs: List[Markup_Tree]): Markup_Tree = new Markup_Tree(node, bs)
    1.28 +
    1.29 +  private def add(branch: Markup_Tree) =   // FIXME avoid sort
    1.30 +    set_branches((branch :: branches) sort ((a, b) => a.node.start < b.node.start))
    1.31 +
    1.32 +  private def remove(bs: List[Markup_Tree]) = set_branches(branches -- bs)
    1.33 +
    1.34 +  def + (new_tree: Markup_Tree): Markup_Tree =
    1.35 +  {
    1.36 +    val new_node = new_tree.node
    1.37 +    if (new_node fits_into node) {
    1.38 +      var inserted = false
    1.39 +      val new_branches =
    1.40 +        branches.map(branch =>
    1.41 +          if ((new_node fits_into branch.node) && !inserted) {
    1.42 +            inserted = true
    1.43 +            branch + new_tree
    1.44 +          }
    1.45 +          else branch)
    1.46 +      if (!inserted) {
    1.47 +        // new_tree did not fit into children of this
    1.48 +        // -> insert between this and its branches
    1.49 +        val fitting = branches filter(_.node fits_into new_node)
    1.50 +        (this remove fitting) add ((new_tree /: fitting)(_ + _))
    1.51 +      }
    1.52 +      else set_branches(new_branches)
    1.53 +    }
    1.54 +    else {
    1.55 +      System.err.println("ignored nonfitting markup: " + new_node)
    1.56 +      this
    1.57 +    }
    1.58 +  }
    1.59 +
    1.60 +  def flatten: List[Markup_Node] =
    1.61 +  {
    1.62 +    var next_x = node.start
    1.63 +    if (branches.isEmpty) List(this.node)
    1.64 +    else {
    1.65 +      val filled_gaps =
    1.66 +        for {
    1.67 +          child <- branches
    1.68 +          markups =
    1.69 +            if (next_x < child.node.start)
    1.70 +              new Markup_Node(next_x, child.node.start, node.info) :: child.flatten
    1.71 +            else child.flatten
    1.72 +          update = (next_x = child.node.stop)
    1.73 +          markup <- markups
    1.74 +        } yield markup
    1.75 +      if (next_x < node.stop)
    1.76 +        filled_gaps + new Markup_Node(next_x, node.stop, node.info)
    1.77 +      else filled_gaps
    1.78 +    }
    1.79 +  }
    1.80 +}
    1.81 +
    1.82 +
    1.83 +class Markup_Text(val markup: List[Markup_Tree], val content: String)
    1.84 +{
    1.85 +  private lazy val root =
    1.86 +    new Markup_Tree(new Markup_Node(0, content.length, None), markup)
    1.87 +
    1.88 +  def + (new_tree: Markup_Tree): Markup_Text =
    1.89 +    new Markup_Text((root + new_tree).branches, content)
    1.90 +
    1.91 +  def filter(pred: Markup_Node => Boolean): Markup_Text =
    1.92 +  {
    1.93 +    def filt(tree: Markup_Tree): List[Markup_Tree] =
    1.94 +    {
    1.95 +      val branches = tree.branches.flatMap(filt(_))
    1.96 +      if (pred(tree.node)) List(tree.set_branches(branches))
    1.97 +      else branches
    1.98 +    }
    1.99 +    new Markup_Text(markup.flatMap(filt(_)), content)
   1.100 +  }
   1.101 +
   1.102 +  def flatten: List[Markup_Node] = markup.flatten(_.flatten)
   1.103 +
   1.104 +  def swing_tree(swing_node: Markup_Node => DefaultMutableTreeNode): DefaultMutableTreeNode =
   1.105 +  {
   1.106 +    def swing(tree: Markup_Tree): DefaultMutableTreeNode =
   1.107 +    {
   1.108 +      val node = swing_node(tree.node)
   1.109 +      tree.branches foreach ((branch: Markup_Tree) => node.add(swing(branch)))
   1.110 +      node
   1.111 +    }
   1.112 +    swing(root)
   1.113 +  }
   1.114 +}