equal
deleted
inserted
replaced
45 |
45 |
46 /* auxiliary operations */ |
46 /* auxiliary operations */ |
47 |
47 |
48 def next(elem: A): Option[A] = rep.nexts.get(elem) |
48 def next(elem: A): Option[A] = rep.nexts.get(elem) |
49 def prev(elem: A): Option[A] = rep.prevs.get(elem) |
49 def prev(elem: A): Option[A] = rep.prevs.get(elem) |
|
50 |
|
51 def get_after(hook: Option[A]): Option[A] = |
|
52 hook match { |
|
53 case None => rep.start |
|
54 case Some(elem) => next(elem) |
|
55 } |
50 |
56 |
51 def insert_after(hook: Option[A], elem: A): Linear_Set[A] = |
57 def insert_after(hook: Option[A], elem: A): Linear_Set[A] = |
52 if (contains(elem)) throw new Linear_Set.Duplicate(elem.toString) |
58 if (contains(elem)) throw new Linear_Set.Duplicate(elem.toString) |
53 else |
59 else |
54 hook match { |
60 hook match { |