author | wenzelm |
Sun, 22 Aug 2010 22:09:14 +0200 | |
changeset 38583 | ff7f9510b0d6 |
parent 38448 | 62d16c415019 |
child 42718 | d7b2625c1193 |
permissions | -rw-r--r-- |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Pure/General/linear_set.scala |
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
3 |
Author: Fabian Immler, TU Munich |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
4 |
|
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
5 |
Sets with canonical linear order, or immutable linked-lists. |
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
6 |
*/ |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
7 |
|
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
8 |
package isabelle |
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
9 |
|
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
10 |
import scala.collection.SetLike |
36781 | 11 |
import scala.collection.generic.{ImmutableSetFactory, CanBuildFrom, |
12 |
GenericSetTemplate, GenericCompanion} |
|
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
13 |
|
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
14 |
|
36781 | 15 |
object Linear_Set extends ImmutableSetFactory[Linear_Set] |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
16 |
{ |
32465 | 17 |
private case class Rep[A]( |
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
18 |
val start: Option[A], val end: Option[A], val nexts: Map[A, A], prevs: Map[A, A]) |
32465 | 19 |
|
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
20 |
private def empty_rep[A] = Rep[A](None, None, Map(), Map()) |
32465 | 21 |
|
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
22 |
private def make[A](start: Option[A], end: Option[A], nexts: Map[A, A], prevs: Map[A, A]) |
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
23 |
: Linear_Set[A] = new Linear_Set[A] { override val rep = Rep(start, end, nexts, prevs) } |
32465 | 24 |
|
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
25 |
implicit def canBuildFrom[A]: CanBuildFrom[Coll, A, Linear_Set[A]] = setCanBuildFrom[A] |
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
26 |
override def empty[A] = new Linear_Set[A] |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
27 |
|
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
28 |
class Duplicate[A](x: A) extends Exception |
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
29 |
class Undefined[A](x: A) extends Exception |
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
30 |
class Next_Undefined[A](x: Option[A]) extends Exception |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
31 |
} |
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
32 |
|
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
33 |
|
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
34 |
class Linear_Set[A] |
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
35 |
extends scala.collection.immutable.Set[A] |
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
36 |
with GenericSetTemplate[A, Linear_Set] |
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
37 |
with SetLike[A, Linear_Set[A]] |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
38 |
{ |
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
39 |
override def companion: GenericCompanion[Linear_Set] = Linear_Set |
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
40 |
|
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
41 |
|
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
42 |
/* representation */ |
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
43 |
|
32465 | 44 |
protected val rep = Linear_Set.empty_rep[A] |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
45 |
|
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
46 |
|
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
47 |
/* relative addressing */ |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
48 |
|
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
49 |
// FIXME check definedness?? |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
50 |
def next(elem: A): Option[A] = rep.nexts.get(elem) |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
51 |
def prev(elem: A): Option[A] = rep.prevs.get(elem) |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
52 |
|
38368 | 53 |
def get_after(hook: Option[A]): Option[A] = |
54 |
hook match { |
|
55 |
case None => rep.start |
|
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
56 |
case Some(elem) => |
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
57 |
if (!contains(elem)) throw new Linear_Set.Undefined(elem) |
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
58 |
next(elem) |
38368 | 59 |
} |
60 |
||
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
61 |
def insert_after(hook: Option[A], elem: A): Linear_Set[A] = |
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
62 |
if (contains(elem)) throw new Linear_Set.Duplicate(elem) |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
63 |
else |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
64 |
hook match { |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
65 |
case None => |
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
66 |
rep.start match { |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
67 |
case None => Linear_Set.make(Some(elem), Some(elem), Map(), Map()) |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
68 |
case Some(elem1) => |
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
69 |
Linear_Set.make(Some(elem), rep.end, |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
70 |
rep.nexts + (elem -> elem1), rep.prevs + (elem1 -> elem)) |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
71 |
} |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
72 |
case Some(elem1) => |
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
73 |
if (!contains(elem1)) throw new Linear_Set.Undefined(elem1) |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
74 |
else |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
75 |
rep.nexts.get(elem1) match { |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
76 |
case None => |
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
77 |
Linear_Set.make(rep.start, Some(elem), |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
78 |
rep.nexts + (elem1 -> elem), rep.prevs + (elem -> elem1)) |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
79 |
case Some(elem2) => |
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
80 |
Linear_Set.make(rep.start, rep.end, |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
81 |
rep.nexts + (elem1 -> elem) + (elem -> elem2), |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
82 |
rep.prevs + (elem2 -> elem) + (elem -> elem1)) |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
83 |
} |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
84 |
} |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
85 |
|
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
86 |
def delete_after(hook: Option[A]): Linear_Set[A] = |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
87 |
hook match { |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
88 |
case None => |
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
89 |
rep.start match { |
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
90 |
case None => throw new Linear_Set.Next_Undefined[A](None) |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
91 |
case Some(elem1) => |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
92 |
rep.nexts.get(elem1) match { |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
93 |
case None => empty |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
94 |
case Some(elem2) => |
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
95 |
Linear_Set.make(Some(elem2), rep.end, rep.nexts - elem1, rep.prevs - elem2) |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
96 |
} |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
97 |
} |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
98 |
case Some(elem1) => |
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
99 |
if (!contains(elem1)) throw new Linear_Set.Undefined(elem1) |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
100 |
else |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
101 |
rep.nexts.get(elem1) match { |
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
102 |
case None => throw new Linear_Set.Next_Undefined(Some(elem1)) |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
103 |
case Some(elem2) => |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
104 |
rep.nexts.get(elem2) match { |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
105 |
case None => |
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
106 |
Linear_Set.make(rep.start, Some(elem1), rep.nexts - elem1, rep.prevs - elem2) |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
107 |
case Some(elem3) => |
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
108 |
Linear_Set.make(rep.start, rep.end, |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
109 |
rep.nexts - elem2 + (elem1 -> elem3), |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
110 |
rep.prevs - elem2 + (elem3 -> elem1)) |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
111 |
} |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
112 |
} |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
113 |
} |
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
114 |
|
32577
892ebdaf19b4
added append_after (tuned version of former insert_after of Seq);
wenzelm
parents:
32576
diff
changeset
|
115 |
def append_after(hook: Option[A], elems: Seq[A]): Linear_Set[A] = |
37185
64da21a2c6c7
avoid :\ which is not tail-recursive and tends to overflow the tiny JVM stack, which is not resizable at runtime;
wenzelm
parents:
37072
diff
changeset
|
116 |
((hook, this) /: elems) { |
64da21a2c6c7
avoid :\ which is not tail-recursive and tends to overflow the tiny JVM stack, which is not resizable at runtime;
wenzelm
parents:
37072
diff
changeset
|
117 |
case ((last_elem, set), elem) => (Some(elem), set.insert_after(last_elem, elem)) |
64da21a2c6c7
avoid :\ which is not tail-recursive and tends to overflow the tiny JVM stack, which is not resizable at runtime;
wenzelm
parents:
37072
diff
changeset
|
118 |
}._2 |
32577
892ebdaf19b4
added append_after (tuned version of former insert_after of Seq);
wenzelm
parents:
32576
diff
changeset
|
119 |
|
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
120 |
def delete_between(from: Option[A], to: Option[A]): Linear_Set[A] = |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
121 |
{ |
32591 | 122 |
if (isEmpty) this |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
123 |
else { |
32465 | 124 |
val next = |
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
125 |
if (from == rep.end) None |
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
126 |
else if (from == None) rep.start |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
127 |
else from.map(rep.nexts(_)) |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
128 |
if (next == to) this |
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
129 |
else delete_after(from).delete_between(from, to) |
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
130 |
} |
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
131 |
} |
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
132 |
|
32465 | 133 |
|
134 |
/* Set methods */ |
|
135 |
||
136 |
override def stringPrefix = "Linear_Set" |
|
137 |
||
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
138 |
override def isEmpty: Boolean = !rep.start.isDefined |
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
139 |
override def size: Int = if (isEmpty) 0 else rep.nexts.size + 1 |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
140 |
|
34304 | 141 |
def contains(elem: A): Boolean = |
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
142 |
!isEmpty && (rep.end.get == elem || rep.nexts.isDefinedAt(elem)) |
34304 | 143 |
|
37070 | 144 |
private def make_iterator(start: Option[A], which: Map[A, A]): Iterator[A] = new Iterator[A] { |
34304 | 145 |
private var next_elem = start |
38583 | 146 |
def hasNext(): Boolean = next_elem.isDefined |
147 |
def next(): A = |
|
34301 | 148 |
next_elem match { |
149 |
case Some(elem) => |
|
37070 | 150 |
next_elem = which.get(elem) |
34301 | 151 |
elem |
38583 | 152 |
case None => Iterator.empty.next() |
34301 | 153 |
} |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
154 |
} |
32465 | 155 |
|
37070 | 156 |
override def iterator: Iterator[A] = make_iterator(rep.start, rep.nexts) |
34304 | 157 |
|
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
158 |
def iterator(elem: A): Iterator[A] = |
37070 | 159 |
if (contains(elem)) make_iterator(Some(elem), rep.nexts) |
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
160 |
else throw new Linear_Set.Undefined(elem) |
37070 | 161 |
|
37072
9105c8237c7a
renamed "rev" to "reverse" following usual Scala conventions;
wenzelm
parents:
37070
diff
changeset
|
162 |
def reverse_iterator(elem: A): Iterator[A] = |
37070 | 163 |
if (contains(elem)) make_iterator(Some(elem), rep.prevs) |
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
164 |
else throw new Linear_Set.Undefined(elem) |
32465 | 165 |
|
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
166 |
def + (elem: A): Linear_Set[A] = insert_after(rep.end, elem) |
32465 | 167 |
|
168 |
def - (elem: A): Linear_Set[A] = |
|
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
169 |
if (!contains(elem)) throw new Linear_Set.Undefined(elem) |
32465 | 170 |
else delete_after(prev(elem)) |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
171 |
} |