# HG changeset patch
# User immler@in.tum.de
# Date 1237464592 -3600
# Node ID 690927d66d8c893c2daba39d43343f16686918ab
# Parent  aaafe9c4180b3a9fd996713a0cab9bae77b23686
LinearSet.prev

diff -r aaafe9c4180b -r 690927d66d8c src/Tools/jEdit/src/utils/LinearSet.scala
--- 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