This commit was manufactured by cvs2svn to create tag 'v0_0_2'.

[helm.git] / helm / interface / getter.ml

diff --git a/helm/interface/getter.ml b/helm/interface/getter.ml
index d79f395141c0b99ba5c8870e45836bdd14cda128..85e64117b6be0fe66366d4eaea95c811364e8617 100644 (file)
--- a/helm/interface/getter.ml
+++ b/helm/interface/getter.ml
@@ -54,7 +54,12 @@ let read_index url =
    let uris = ref [] in
     try
      while true do
-      uris := (input_line fd) :: !uris
+      let (uri,comp) =
+       match (Str.split (Str.regexp "[ \t]+") (input_line fd)) with
+         [uri] -> (uri,"")
+       | [uri;comp] -> (uri,".gz")
+      in
+       uris := (uri,comp) :: !uris
      done ;
      [] (* only to make the compiler happy *)
     with
@@ -70,14 +75,14 @@ let rec mk_urls_of_uris =
   | he::tl ->
      let map = mk_urls_of_uris tl in
       let uris = read_index he in
-       let url_of_uri uri =
-        let url = uri  ^ ".xml" in
+       let url_of_uri (uri,comp) =
+        let url = uri  ^ ".xml" ^ comp in
          let url' = Str.replace_first (Str.regexp "cic:") he url in
          let url'' = Str.replace_first (Str.regexp "theory:") he url' in
           url''
        in
         List.fold_right
-         (fun uri m -> MapOfStrings.add uri (url_of_uri uri) m)
+         (fun (uri,comp) m -> MapOfStrings.add uri (url_of_uri (uri,comp)) m)
          uris map
 ;;