aboutsummaryrefslogtreecommitdiff
path: root/library/goptions.ml
diff options
context:
space:
mode:
authorGaëtan Gilbert2019-06-03 14:32:18 +0200
committerGaëtan Gilbert2019-06-03 14:32:18 +0200
commit4541d28ba3c50bc8e45c4ccf418bbdd225454dec (patch)
tree2e308e2f0d081519f608969152b309e7922f2637 /library/goptions.ml
parent7032085c809993d6a173e51aec447c02828ae070 (diff)
Expose set interface to option tables
This lets us avoid having to cache the SearchBlacklist.elements call in search as we can just use the set module's for_all function.
Diffstat (limited to 'library/goptions.ml')
-rw-r--r--library/goptions.ml19
1 files changed, 10 insertions, 9 deletions
diff --git a/library/goptions.ml b/library/goptions.ml
index f4b8ce9465..2798c21c81 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -53,9 +53,9 @@ module MakeTable =
functor
(A : sig
type t
- type key
- val compare : t -> t -> int
- val table : (string * key table_of_A) list ref
+ type key
+ module Set : CSig.SetS with type elt = t
+ val table : (string * key table_of_A) list ref
val encode : Environ.env -> key -> t
val subst : substitution -> t -> t
val printer : t -> Pp.t
@@ -74,7 +74,7 @@ module MakeTable =
if String.List.mem_assoc nick !A.table then
user_err Pp.(str "Sorry, this table name (" ++ str nick ++ str ") is already used.")
- module MySet = Set.Make (struct type t = A.t let compare = A.compare end)
+ module MySet = A.Set
let t = Summary.ref MySet.empty ~name:nick
@@ -119,8 +119,9 @@ module MakeTable =
}
let _ = A.table := (nick, table_of_A)::!A.table
- let active c = MySet.mem c !t
- let elements () = MySet.elements !t
+
+ let v () = !t
+ let active x = A.Set.mem x !t
end
let string_table = ref []
@@ -138,7 +139,7 @@ module StringConvert = functor (A : StringConvertArg) ->
struct
type t = string
type key = string
- let compare = String.compare
+ module Set = CString.Set
let table = string_table
let encode _env x = x
let subst _ x = x
@@ -158,7 +159,7 @@ let get_ref_table k = String.List.assoc (nickname k) !ref_table
module type RefConvertArg =
sig
type t
- val compare : t -> t -> int
+ module Set : CSig.SetS with type elt = t
val encode : Environ.env -> qualid -> t
val subst : substitution -> t -> t
val printer : t -> Pp.t
@@ -171,7 +172,7 @@ module RefConvert = functor (A : RefConvertArg) ->
struct
type t = A.t
type key = qualid
- let compare = A.compare
+ module Set = A.Set
let table = ref_table
let encode = A.encode
let subst = A.subst