# HG changeset patch
# User immler@in.tum.de
# Date 1236246827 -3600
# Node ID de629c23b38930e23ab6ad9dc6b5729ed3185d94
# Parent  f0e55d9ffe45da788f11d23bc9811319eee0b661
implemented delete_after

diff -r f0e55d9ffe45 -r de629c23b389 src/Tools/jEdit/src/utils/LinearSet.scala
--- a/src/Tools/jEdit/src/utils/LinearSet.scala	Thu Mar 05 10:13:25 2009 +0100
+++ b/src/Tools/jEdit/src/utils/LinearSet.scala	Thu Mar 05 10:53:47 2009 +0100
@@ -55,9 +55,22 @@
     
   def +(elem: A): LinearSet[A] = insert_after(last_elem, elem)
 
+  def delete_after(elem: Option[A]): LinearSet[A] =
+    elem match {
+      case Some(elem) =>
+        if (!contains(elem)) throw new LinearSet.Undefined(elem.toString)
+        else if (!body.isDefinedAt(elem)) throw new LinearSet.Undefined(null)
+        else if (body(elem) == last_elem.get) LinearSet.make(first_elem, Some(elem), body - elem)
+        else LinearSet.make(first_elem, last_elem, body - elem - body(elem) + (elem -> body(body(elem))))
+      case None =>
+        if (isEmpty) throw new LinearSet.Undefined(null)
+        else if (size == 1) empty
+        else LinearSet.make(Some(body(first_elem.get)), last_elem, body - first_elem.get)
+    }
+    
   def -(elem: A): LinearSet[A] =
     if (!contains(elem)) throw new LinearSet.Undefined(elem.toString)
-    else error("FIXME")
+    else delete_after(body find (p => p._2 == elem) map (p => p._1))
 
   def elements = new Iterator[A] {
     private var next_elem = first_elem