src/Tools/jEdit/src/prover/MarkupNode.scala
changeset 34717 3f32e08bbb6c
parent 34708 611864f2729d
     1.1 --- a/src/Tools/jEdit/src/prover/MarkupNode.scala	Sun Sep 06 16:21:01 2009 +0200
     1.2 +++ b/src/Tools/jEdit/src/prover/MarkupNode.scala	Sun Sep 06 22:27:32 2009 +0200
     1.3 @@ -12,78 +12,100 @@
     1.4  import isabelle.proofdocument.ProofDocument
     1.5  
     1.6  
     1.7 -class MarkupNode(val start: Int, val stop: Int, val content: String, val info: Any,
     1.8 -  val children: List[MarkupNode])
     1.9 +class Markup_Node(val start: Int, val stop: Int, val info: Any)
    1.10  {
    1.11 +  def fits_into(that: Markup_Node): Boolean =
    1.12 +    that.start <= this.start && this.stop <= that.stop
    1.13 +}
    1.14 +
    1.15  
    1.16 -  def swing_tree(make_node: MarkupNode => DefaultMutableTreeNode): DefaultMutableTreeNode =
    1.17 -  {
    1.18 -    val node = make_node(this)
    1.19 -    children.foreach(node add _.swing_tree(make_node))
    1.20 -    node
    1.21 -  }
    1.22 +class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree])
    1.23 +{
    1.24 +  def set_branches(bs: List[Markup_Tree]): Markup_Tree = new Markup_Tree(node, bs)
    1.25  
    1.26 -  def set_children(new_children: List[MarkupNode]): MarkupNode =
    1.27 -    new MarkupNode(start, stop, content, info, new_children)
    1.28 +  private def add(branch: Markup_Tree) =   // FIXME avoid sort
    1.29 +    set_branches((branch :: branches) sort ((a, b) => a.node.start < b.node.start))
    1.30  
    1.31 -  private def add(child: MarkupNode) =   // FIXME avoid sort?
    1.32 -    set_children ((child :: children) sort ((a, b) => a.start < b.start))
    1.33 -
    1.34 -  def remove(nodes: List[MarkupNode]) = set_children(children -- nodes)
    1.35 +  private def remove(bs: List[Markup_Tree]) = set_branches(branches -- bs)
    1.36  
    1.37 -  def fits_into(node: MarkupNode): Boolean =
    1.38 -    node.start <= this.start && this.stop <= node.stop
    1.39 -
    1.40 -  def + (new_child: MarkupNode): MarkupNode =
    1.41 +  def + (new_tree: Markup_Tree): Markup_Tree =
    1.42    {
    1.43 -    if (new_child fits_into this) {
    1.44 +    val new_node = new_tree.node
    1.45 +    if (new_node fits_into node) {
    1.46        var inserted = false
    1.47 -      val new_children =
    1.48 -        children.map(c =>
    1.49 -          if ((new_child fits_into c) && !inserted) {inserted = true; c + new_child}
    1.50 -          else c)
    1.51 +      val new_branches =
    1.52 +        branches.map(branch =>
    1.53 +          if ((new_node fits_into branch.node) && !inserted) {
    1.54 +            inserted = true
    1.55 +            branch + new_tree
    1.56 +          }
    1.57 +          else branch)
    1.58        if (!inserted) {
    1.59 -        // new_child did not fit into children of this
    1.60 -        // -> insert new_child between this and its children
    1.61 -        val fitting = children filter(_ fits_into new_child)
    1.62 -        (this remove fitting) add ((new_child /: fitting) (_ + _))
    1.63 +        // new_tree did not fit into children of this
    1.64 +        // -> insert between this and its branches
    1.65 +        val fitting = branches filter(_.node fits_into new_node)
    1.66 +        (this remove fitting) add ((new_tree /: fitting)(_ + _))
    1.67        }
    1.68 -      else this set_children new_children
    1.69 +      else set_branches(new_branches)
    1.70      }
    1.71      else {
    1.72 -      System.err.println("ignored nonfitting markup: " + new_child)
    1.73 +      System.err.println("ignored nonfitting markup: " + new_node)
    1.74        this
    1.75      }
    1.76    }
    1.77  
    1.78 -  def flatten: List[MarkupNode] = {
    1.79 -    var next_x = start
    1.80 -    if (children.isEmpty) List(this)
    1.81 +  def flatten: List[Markup_Node] =
    1.82 +  {
    1.83 +    var next_x = node.start
    1.84 +    if (branches.isEmpty) List(this.node)
    1.85      else {
    1.86 -      val filled_gaps = for {
    1.87 -        child <- children
    1.88 -        markups =
    1.89 -          if (next_x < child.start) {
    1.90 -            // FIXME proper content!?
    1.91 -            new MarkupNode(next_x, child.start, content, info, Nil) :: child.flatten
    1.92 -          }
    1.93 -          else child.flatten
    1.94 -        update = (next_x = child.stop)
    1.95 -        markup <- markups
    1.96 -      } yield markup
    1.97 -      if (next_x < stop)
    1.98 -        filled_gaps + new MarkupNode(next_x, stop, content, info, Nil) // FIXME proper content!?
    1.99 +      val filled_gaps =
   1.100 +        for {
   1.101 +          child <- branches
   1.102 +          markups =
   1.103 +            if (next_x < child.node.start)
   1.104 +              new Markup_Node(next_x, child.node.start, node.info) :: child.flatten
   1.105 +            else child.flatten
   1.106 +          update = (next_x = child.node.stop)
   1.107 +          markup <- markups
   1.108 +        } yield markup
   1.109 +      if (next_x < node.stop)
   1.110 +        filled_gaps + new Markup_Node(next_x, node.stop, node.info)
   1.111        else filled_gaps
   1.112      }
   1.113    }
   1.114 +}
   1.115  
   1.116 -  def filter(p: MarkupNode => Boolean): List[MarkupNode] =
   1.117 +
   1.118 +class Markup_Text(val markup: List[Markup_Tree], val content: String)
   1.119 +{
   1.120 +  private lazy val root =
   1.121 +    new Markup_Tree(new Markup_Node(0, content.length, None), markup)
   1.122 +
   1.123 +  def + (new_tree: Markup_Tree): Markup_Text =
   1.124 +    new Markup_Text((root + new_tree).branches, content)
   1.125 +
   1.126 +  def filter(pred: Markup_Node => Boolean): Markup_Text =
   1.127    {
   1.128 -    val filtered = children.flatMap(_.filter(p))
   1.129 -    if (p(this)) List(this set_children(filtered))
   1.130 -    else filtered
   1.131 +    def filt(tree: Markup_Tree): List[Markup_Tree] =
   1.132 +    {
   1.133 +      val branches = tree.branches.flatMap(filt(_))
   1.134 +      if (pred(tree.node)) List(tree.set_branches(branches))
   1.135 +      else branches
   1.136 +    }
   1.137 +    new Markup_Text(markup.flatMap(filt(_)), content)
   1.138    }
   1.139  
   1.140 -  override def toString =
   1.141 -    "([" + start + " - " + stop + "] ( " + content + "): " + info.toString
   1.142 +  def flatten: List[Markup_Node] = markup.flatten(_.flatten)
   1.143 +
   1.144 +  def swing_tree(swing_node: Markup_Node => DefaultMutableTreeNode): DefaultMutableTreeNode =
   1.145 +  {
   1.146 +    def swing(tree: Markup_Tree): DefaultMutableTreeNode =
   1.147 +    {
   1.148 +      val node = swing_node(tree.node)
   1.149 +      tree.branches foreach ((branch: Markup_Tree) => node.add(swing(branch)))
   1.150 +      node
   1.151 +    }
   1.152 +    swing(root)
   1.153 +  }
   1.154  }