]> matita.cs.unibo.it Git - helm.git/commitdiff
added keys method that list currently loaded stylesheets' keys
authorStefano Zacchiroli <zack@upsilon.cc>
Tue, 25 Mar 2003 15:42:06 +0000 (15:42 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Tue, 25 Mar 2003 15:42:06 +0000 (15:42 +0000)
helm/uwobo/uwobo_styles.ml
helm/uwobo/uwobo_styles.mli

index d866ede5d42136764ae69880b761b3f99fa4cae3..4fb2cbf31a63ab6c205493846500d89476c2f3c9 100644 (file)
@@ -109,6 +109,8 @@ class styles =
 
     (* stylesheets usage *)
 
+    method keys = List.map fst uris
+
     method list =
       List.map
         (fun (key, uri) ->
index 9d03b0924ba5ed64579e4de3e6b6cfa8398916ef..7b2fa171e31f0b47a32a67d5c5f36b9563cd3b32 100644 (file)
@@ -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 *)