in
(* now calculate the list of objects that belong to these baseuris *)
let uri_to_remove =
- List.fold_left
- (fun acc buri ->
- let inhabitants = HG.ls (buri ^ "/") in
- let inhabitants = List.filter
- (function HGT.Ls_object _ -> true | _ -> false)
- inhabitants
- in
- let inhabitants = List.map
- (function
- | HGT.Ls_object e -> buri ^ "/" ^ e.HGT.uri
- | _ -> assert false)
- inhabitants
- in
- inhabitants @ acc)
- [] buri_to_remove
+ try
+ List.fold_left
+ (fun acc buri ->
+ let inhabitants = HG.ls (buri ^ "/") in
+ let inhabitants = List.filter
+ (function HGT.Ls_object _ -> true | _ -> false)
+ inhabitants
+ in
+ let inhabitants = List.map
+ (function
+ | HGT.Ls_object e -> buri ^ "/" ^ e.HGT.uri
+ | _ -> assert false)
+ inhabitants
+ in
+ inhabitants @ acc)
+ [] buri_to_remove
+ with HGT.Invalid_URI u ->
+ MatitaLog.error ("We were listing an invalid buri: " ^ u);
+ exit 1
in
(* now we want the list of all uri that depend on them *)
let depend =
List.iter
(fun stm ->
match baseuri_of_baseuri_decl stm with
- | Some buri -> uri := MatitaMisc.strip_trailing_slash buri
+ | Some buri ->
+ let u = MatitaMisc.strip_trailing_slash buri in
+ if String.length u < 5 || String.sub u 0 5 <> "cic:/" then
+ MatitaLog.error (file ^ " sets an incorrect baseuri: " ^ buri);
+ (try
+ ignore(HG.resolve u)
+ with
+ | HGT.Unresolvable_URI _ ->
+ MatitaLog.error (file ^ " sets an unresolvable baseuri: "^buri)
+ | HGT.Key_not_found _ -> ());
+ uri := u
| None -> ())
stms;
!uri