# HG changeset patch
# User wenzelm
# Date 1281713728 -7200
# Node ID 07bc80bdeebc3943b9c2acbd9bf4c421d7c29c0b
# Parent  f7d2574dc3a639c2d8ab2b4fe7aeaf8c243297e6
added get_after convenience;

diff -r f7d2574dc3a6 -r 07bc80bdeebc src/Pure/General/linear_set.scala
--- 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