src/Pure/PIDE/markup_node.scala

 
 import javax.swing.tree.DefaultMutableTreeNode
 
 
 
-class Markup_Node(val start: Int, val stop: Int, val info: Any)
+case class Markup_Node(val start: Int, val stop: Int, val info: Any)
 {
   def fits_into(that: Markup_Node): Boolean =
     that.start <= this.start && this.stop <= that.stop
 }
 
 
-class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree])
+case class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree])
 {
-  def set_branches(bs: List[Markup_Tree]): Markup_Tree = new Markup_Tree(node, bs)
+  private def add(branch: Markup_Tree) =   // FIXME avoid sort
+    copy(branches = (branch :: branches).sortWith((a, b) => a.node.start < b.node.start))
 
-  private def add(branch: Markup_Tree) =   // FIXME avoid sort
-    set_branches((branch :: branches).sortWith((a, b) => a.node.start < b.node.start))
-
-  private def remove(bs: List[Markup_Tree]) = set_branches(branches -- bs)
+  private def remove(bs: List[Markup_Tree]) =
+    copy(branches = branches.filterNot(bs.contains(_)))
 
   def + (new_tree: Markup_Tree): Markup_Tree =
   {
     val new_node = new_tree.node
     if (new_node fits_into node) {

         // new_tree did not fit into children of this
         // -> insert between this and its branches
         val fitting = branches filter(_.node fits_into new_node)
         (this remove fitting) add ((new_tree /: fitting)(_ + _))
       }
-      else set_branches(new_branches)
+      else copy(branches = new_branches)
     }
     else {
       System.err.println("ignored nonfitting markup: " + new_node)
       this
     }

     }
   }
 }
 
 
-class Markup_Text(val markup: List[Markup_Tree], val content: String)
+case class Markup_Text(val markup: List[Markup_Tree], val content: String)
 {
   private lazy val root =
     new Markup_Tree(new Markup_Node(0, content.length, None), markup)
 
   def + (new_tree: Markup_Tree): Markup_Text =

   def filter(pred: Markup_Node => Boolean): Markup_Text =
   {
     def filt(tree: Markup_Tree): List[Markup_Tree] =
     {
       val branches = tree.branches.flatMap(filt(_))
-      if (pred(tree.node)) List(tree.set_branches(branches))
+      if (pred(tree.node)) List(tree.copy(branches = branches))
       else branches
     }
     new Markup_Text(markup.flatMap(filt(_)), content)
   }