open Printf ;;
-let clean_owner_environment dbd owner =
+let xpointer_RE = Pcre.regexp "#.*$"
+
+let clean_owner_environment () =
+ let dbd = MatitaMisc.dbd_instance () in
+ let owner = (Helm_registry.get "matita.owner") in
let obj_tbl = MetadataTypes.obj_tbl () in
let sort_tbl = MetadataTypes.sort_tbl () in
let rel_tbl = MetadataTypes.rel_tbl () in
DROP INDEX no_concl_hyp_source ON no_concl_hyp (source);
DROP INDEX no_concl_hyp_no ON no_concl_hyp (no);
*)
- (try
- MetadataDb.clean ~dbd
- with
- exn ->
- match Mysql.errno dbd with
- | Mysql.No_such_table -> ()
- | _ -> raise exn
- | _ -> ()
- );
+ let owned_uris =
+ try
+ MetadataDb.clean ~dbd
+ with Mysql.Error _ as exn ->
+ match Mysql.errno dbd with
+ | Mysql.No_such_table -> []
+ | _ -> raise exn
+ in
+ List.iter
+ (fun uri ->
+ let uri = Pcre.replace ~rex:xpointer_RE ~templ:"" uri in
+ List.iter
+ (fun suffix -> Http_getter.unregister (uri ^ suffix))
+ [""; ".body"; ".types"])
+ owned_uris;
List.iter (fun statement ->
try
ignore (Mysql.exec dbd statement)
- with
- exn ->
- match Mysql.errno dbd with
- | Mysql.No_such_table -> ()
- | _ -> raise exn
- | _ -> ()
- ) statements
+ with Mysql.Error _ as exn ->
+ match Mysql.errno dbd with
+ | Mysql.Bad_table_error -> ()
+ | _ -> raise exn
+ ) statements;
;;
-let create_owner_environment dbd owner =
+let create_owner_environment () =
+ let dbd = MatitaMisc.dbd_instance () in
+ let owner = (Helm_registry.get "matita.owner") in
let obj_tbl = MetadataTypes.obj_tbl () in
let sort_tbl = MetadataTypes.sort_tbl () in
let rel_tbl = MetadataTypes.rel_tbl () in