--- a/src/Pure/General/linear_set.scala Thu Aug 12 17:55:23 2010 +0200
+++ b/src/Pure/General/linear_set.scala Fri Aug 13 17:35:28 2010 +0200
@@ -48,6 +48,12 @@
def next(elem: A): Option[A] = rep.nexts.get(elem)
def prev(elem: A): Option[A] = rep.prevs.get(elem)
+ def get_after(hook: Option[A]): Option[A] =
+ hook match {
+ case None => rep.start
+ case Some(elem) => next(elem)
+ }
+
def insert_after(hook: Option[A], elem: A): Linear_Set[A] =
if (contains(elem)) throw new Linear_Set.Duplicate(elem.toString)
else