LinearSet.prev

--- a/src/Tools/jEdit/src/utils/LinearSet.scala	Sun Mar 08 23:03:49 2009 +0100
+++ b/src/Tools/jEdit/src/utils/LinearSet.scala	Thu Mar 19 13:09:52 2009 +0100
@@ -34,7 +34,7 @@
   /* basic methods */
 
   def next(elem: A) = body.get(elem)
-  
+  def prev(elem: A) = body.find(_._2 == elem).map(_._2)
   override def isEmpty: Boolean = !last_elem.isDefined
   def size: Int = if (isEmpty) 0 else body.size + 1