From fc967a62e29b445633102bc1d65ab7645405e288 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 25 Mar 2003 15:42:06 +0000 Subject: [PATCH] added keys method that list currently loaded stylesheets' keys --- helm/uwobo/uwobo_styles.ml | 2 ++ helm/uwobo/uwobo_styles.mli | 3 +++ 2 files changed, 5 insertions(+) diff --git a/helm/uwobo/uwobo_styles.ml b/helm/uwobo/uwobo_styles.ml index d866ede5d..4fb2cbf31 100644 --- a/helm/uwobo/uwobo_styles.ml +++ b/helm/uwobo/uwobo_styles.ml @@ -109,6 +109,8 @@ class styles = (* stylesheets usage *) + method keys = List.map fst uris + method list = List.map (fun (key, uri) -> diff --git a/helm/uwobo/uwobo_styles.mli b/helm/uwobo/uwobo_styles.mli index 9d03b0924..7b2fa171e 100644 --- a/helm/uwobo/uwobo_styles.mli +++ b/helm/uwobo/uwobo_styles.mli @@ -62,6 +62,9 @@ class styles: (** {2 Stylesheets usage} *) + (** @return the list of currently loaded stylesheets' keys *) + method keys: string list + (** @return a list of strings, each string is a textual representation of information related to a loaded stylesheet. This representation includes at least stylesheet's key and URI *) -- 2.39.2