src/Tools/jEdit/src/prover/MarkupNode.scala
changeset 34759 bfea7839d9e1
parent 34758 710e3a9a4c95
child 34760 dc7f5e0d9d27
     1.1 --- a/src/Tools/jEdit/src/prover/MarkupNode.scala	Tue Dec 08 14:29:29 2009 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,111 +0,0 @@
     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 -}