author | wenzelm |
Sun, 26 Feb 2012 19:20:46 +0100 | |
changeset 46686 | b2ae19322ff8 |
parent 46621 | 7a8dd77c9f93 |
child 46712 | 8650d9a95736 |
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 |
46686 | 2 |
Module: PIDE |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
3 |
Author: Makarius |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
4 |
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
|
5 |
|
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
6 |
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
|
7 |
*/ |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
8 |
|
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
9 |
package isabelle |
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
10 |
|
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
11 |
import scala.collection.SetLike |
36781 | 12 |
import scala.collection.generic.{ImmutableSetFactory, CanBuildFrom, |
13 |
GenericSetTemplate, GenericCompanion} |
|
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
14 |
|
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
15 |
|
36781 | 16 |
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
|
17 |
{ |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
18 |
private val empty_val: Linear_Set[Nothing] = new Linear_Set[Nothing](None, None, Map(), Map()) |
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
19 |
override def empty[A] = empty_val.asInstanceOf[Linear_Set[A]] |
32465 | 20 |
|
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
21 |
implicit def canBuildFrom[A]: CanBuildFrom[Coll, A, Linear_Set[A]] = setCanBuildFrom[A] |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
22 |
|
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
23 |
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
|
24 |
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
|
25 |
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
|
26 |
} |
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
27 |
|
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
28 |
|
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
29 |
class Linear_Set[A] private( |
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
30 |
start: Option[A], end: Option[A], val nexts: Map[A, A], prevs: Map[A, A]) |
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
31 |
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
|
32 |
with GenericSetTemplate[A, Linear_Set] |
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
33 |
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
|
34 |
{ |
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
35 |
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
|
36 |
|
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
37 |
|
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
38 |
/* relative addressing */ |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
39 |
|
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
40 |
// FIXME check definedness?? |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
41 |
def next(elem: A): Option[A] = nexts.get(elem) |
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
42 |
def prev(elem: A): Option[A] = prevs.get(elem) |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
43 |
|
38368 | 44 |
def get_after(hook: Option[A]): Option[A] = |
45 |
hook match { |
|
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
46 |
case None => start |
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
47 |
case Some(elem) => |
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
48 |
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
|
49 |
next(elem) |
38368 | 50 |
} |
51 |
||
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
52 |
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
|
53 |
if (contains(elem)) throw new Linear_Set.Duplicate(elem) |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
54 |
else |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
55 |
hook match { |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
56 |
case None => |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
57 |
start match { |
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
58 |
case None => new Linear_Set[A](Some(elem), Some(elem), Map(), Map()) |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
59 |
case Some(elem1) => |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
60 |
new Linear_Set[A](Some(elem), end, |
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
61 |
nexts + (elem -> elem1), prevs + (elem1 -> elem)) |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
62 |
} |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
63 |
case Some(elem1) => |
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
64 |
if (!contains(elem1)) throw new Linear_Set.Undefined(elem1) |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
65 |
else |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
66 |
nexts.get(elem1) match { |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
67 |
case None => |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
68 |
new Linear_Set[A](start, Some(elem), |
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
69 |
nexts + (elem1 -> elem), prevs + (elem -> elem1)) |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
70 |
case Some(elem2) => |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
71 |
new Linear_Set[A](start, end, |
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
72 |
nexts + (elem1 -> elem) + (elem -> elem2), |
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
73 |
prevs + (elem2 -> elem) + (elem -> elem1)) |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
74 |
} |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
75 |
} |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
76 |
|
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
77 |
def delete_after(hook: Option[A]): Linear_Set[A] = |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
78 |
hook match { |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
79 |
case None => |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
80 |
start match { |
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
81 |
case None => throw new Linear_Set.Next_Undefined[A](None) |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
82 |
case Some(elem1) => |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
83 |
nexts.get(elem1) match { |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
84 |
case None => empty |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
85 |
case Some(elem2) => |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
86 |
new Linear_Set[A](Some(elem2), end, nexts - elem1, prevs - elem2) |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
87 |
} |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
88 |
} |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
89 |
case Some(elem1) => |
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
90 |
if (!contains(elem1)) throw new Linear_Set.Undefined(elem1) |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
91 |
else |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
92 |
nexts.get(elem1) match { |
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
93 |
case None => throw new Linear_Set.Next_Undefined(Some(elem1)) |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
94 |
case Some(elem2) => |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
95 |
nexts.get(elem2) match { |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
96 |
case None => |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
97 |
new Linear_Set[A](start, Some(elem1), nexts - elem1, prevs - elem2) |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
98 |
case Some(elem3) => |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
99 |
new Linear_Set[A](start, end, |
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
100 |
nexts - elem2 + (elem1 -> elem3), |
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
101 |
prevs - elem2 + (elem3 -> elem1)) |
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
102 |
} |
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
103 |
} |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
104 |
} |
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
105 |
|
32577
892ebdaf19b4
added append_after (tuned version of former insert_after of Seq);
wenzelm
parents:
32576
diff
changeset
|
106 |
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
|
107 |
((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
|
108 |
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
|
109 |
}._2 |
32577
892ebdaf19b4
added append_after (tuned version of former insert_after of Seq);
wenzelm
parents:
32576
diff
changeset
|
110 |
|
32576
20b261654e33
double linking for improved performance of "prev";
wenzelm
parents:
32465
diff
changeset
|
111 |
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
|
112 |
{ |
32591 | 113 |
if (isEmpty) this |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
114 |
else { |
32465 | 115 |
val next = |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
116 |
if (from == end) None |
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
117 |
else if (from == None) start |
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
118 |
else from.map(nexts(_)) |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
119 |
if (next == to) this |
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
120 |
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
|
121 |
} |
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
122 |
} |
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
123 |
|
32465 | 124 |
|
125 |
/* Set methods */ |
|
126 |
||
127 |
override def stringPrefix = "Linear_Set" |
|
128 |
||
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
129 |
override def isEmpty: Boolean = !start.isDefined |
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
130 |
override def size: Int = if (isEmpty) 0 else nexts.size + 1 |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
131 |
|
34304 | 132 |
def contains(elem: A): Boolean = |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
133 |
!isEmpty && (end.get == elem || nexts.isDefinedAt(elem)) |
34304 | 134 |
|
46620 | 135 |
private def make_iterator(from: Option[A], which: Map[A, A]): Iterator[A] = new Iterator[A] { |
136 |
private var next_elem = from |
|
38583 | 137 |
def hasNext(): Boolean = next_elem.isDefined |
138 |
def next(): A = |
|
34301 | 139 |
next_elem match { |
140 |
case Some(elem) => |
|
37070 | 141 |
next_elem = which.get(elem) |
34301 | 142 |
elem |
38583 | 143 |
case None => Iterator.empty.next() |
34301 | 144 |
} |
32464
5b9731f83569
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm
parents:
diff
changeset
|
145 |
} |
32465 | 146 |
|
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
147 |
override def iterator: Iterator[A] = make_iterator(start, nexts) |
34304 | 148 |
|
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34304
diff
changeset
|
149 |
def iterator(elem: A): Iterator[A] = |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
150 |
if (contains(elem)) make_iterator(Some(elem), nexts) |
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
151 |
else throw new Linear_Set.Undefined(elem) |
37070 | 152 |
|
37072
9105c8237c7a
renamed "rev" to "reverse" following usual Scala conventions;
wenzelm
parents:
37070
diff
changeset
|
153 |
def reverse_iterator(elem: A): Iterator[A] = |
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
154 |
if (contains(elem)) make_iterator(Some(elem), prevs) |
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38368
diff
changeset
|
155 |
else throw new Linear_Set.Undefined(elem) |
32465 | 156 |
|
46621
7a8dd77c9f93
streamlined abstract datatype, eliminating odd representation class;
wenzelm
parents:
46620
diff
changeset
|
157 |
def + (elem: A): Linear_Set[A] = insert_after(end, elem) |
32465 | 158 |
|
159 |
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
|
160 |
if (!contains(elem)) throw new Linear_Set.Undefined(elem) |
32465 | 161 |
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
|
162 |
} |