]> matita.cs.unibo.it Git - helm.git/commitdiff
- removed special handling of universes (no longer needed)
authorStefano Zacchiroli <zack@upsilon.cc>
Fri, 4 Feb 2005 15:02:38 +0000 (15:02 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Fri, 4 Feb 2005 15:02:38 +0000 (15:02 +0000)
- removed ancient part of commented code

helm/ocaml/getter/http_getter.ml

index 9afcafebb87e958e48ab00a875a88df3387535a5..f7ca2388c89b9653d04f8087ac4d021fc8d1e966 100644 (file)
@@ -264,16 +264,7 @@ let resolve uri =
   if remote () then
     resolve_remote uri
   else
-    
-    (**** FIXME ******)
-    if is_cic_uri uri && Pcre.pmatch ~pat:"\\.univ$" uri then
-      begin
-       prerr_endline "!!! E' in ~tassi !!!";
-       "file:///home/tassi/mylib" ^ 
-       (String.sub uri 4 ((String.length uri) - 4)) ^ ".xml.gz"
-      end
-    else
-      (map_of_uri uri)#resolve uri
+    (map_of_uri uri)#resolve uri
        
 let register ~uri ~url =
   if remote () then
@@ -500,9 +491,6 @@ let ls =
                  let dir =
                   "theory" ^ String.sub !dir_found 3
                    (String.length !dir_found - 3) ^ ".theory" in
-(*
-prerr_endline ("### " ^ uri ^ " ==> " ^ !dir_found ^ " ==> " ^ dir);
-*)
                  if not (List.mem dir !valid_candidates) then
                  valid_candidates := dir::!valid_candidates
                end
@@ -515,10 +503,6 @@ prerr_endline ("### " ^ uri ^ " ==> " ^ !dir_found ^ " ==> " ^ dir);
              then
               (index_not_generated_yet := false ;
                store_obj "index.theory"));
-(*
-prerr_endline ("@@@ " ^ String.concat " " !valid_candidates);
-prerr_endline ("!!! " ^ String.concat " " (List.map fst !candidates_found));
-*)
       List.iter
        (fun (uri,localpart) ->
          if not (List.mem uri !valid_candidates) then