diff options
| author | Gaëtan Gilbert | 2020-02-24 15:03:08 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-04-13 15:18:18 +0200 |
| commit | 8e3abd852c9a1c65738be63215e94014550f2c5a (patch) | |
| tree | 1cdd4d19b7a1e8cc828cc608ac8c6f56dffebe9e /library | |
| parent | b98ef72ee300e52dd2c67f03da358e3c2102cdbb (diff) | |
correctly open objects for Names filters
Diffstat (limited to 'library')
| -rw-r--r-- | library/libobject.ml | 6 | ||||
| -rw-r--r-- | library/libobject.mli | 2 |
2 files changed, 5 insertions, 3 deletions
diff --git a/library/libobject.ml b/library/libobject.ml index 392a64e5d0..c38e0d891b 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -28,8 +28,6 @@ let simple_open f filter i o = match filter with | Unfiltered -> f i o | Names _ -> () -let todo_filter = simple_open - let filter_and f1 f2 = match f1, f2 with | Unfiltered, f | f, Unfiltered -> Some f | Names n1, Names n2 -> @@ -41,6 +39,10 @@ let filter_or f1 f2 = match f1, f2 with | Unfiltered, f | f, Unfiltered -> Unfiltered | Names n1, Names n2 -> Names (NSet.union n1 n2) +let in_filter_ref gr = function + | Unfiltered -> true + | Names ns -> NSet.mem (Globnames.TrueGlobal gr) ns + type 'a object_declaration = { object_name : string; cache_function : object_name * 'a -> unit; diff --git a/library/libobject.mli b/library/libobject.mli index 27b47264a6..1c82349bb6 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -92,7 +92,7 @@ val filter_and : open_filter -> open_filter -> open_filter option val filter_or : open_filter -> open_filter -> open_filter -val todo_filter : (int -> object_name * 'a -> unit) -> open_filter -> int -> object_name * 'a -> unit +val in_filter_ref : Names.GlobRef.t -> open_filter -> bool (** The default object is a "Keep" object with empty methods. Object creators are advised to use the construction |