From: Stefano Zacchiroli Date: Thu, 10 Feb 2005 15:51:42 +0000 (+0000) Subject: added "unindex" to undo indexing of a single object X-Git-Tag: before_svn_merge~10 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=df29cafb872244de1a6a9b3c273b329a6e15fa8c;p=helm.git added "unindex" to undo indexing of a single object --- diff --git a/helm/ocaml/metadata/metadataDb.ml b/helm/ocaml/metadata/metadataDb.ml index 170d02d77..4b7664c22 100644 --- a/helm/ocaml/metadata/metadataDb.ml +++ b/helm/ocaml/metadata/metadataDb.ml @@ -120,6 +120,9 @@ let index_inductive_def ~dbd = List.iter (fun (uri, name, _) -> insert_name ~dbd ~uri ~name) metadata end +let tables_to_clean = + [sort_tbl; rel_tbl; obj_tbl; conclno_tbl; conclno_hyp_tbl; name_tbl] + let clean ~(dbd:Mysql.dbd) = let owned_uris = (* list of uris in list-of-columns format *) let query = sprintf "SELECT source FROM %s" (obj_tbl ()) in @@ -139,7 +142,16 @@ let clean ~(dbd:Mysql.dbd) = (fun source_col -> ignore (Mysql.exec dbd (query source_col))) owned_uris in - List.iter del_from - [sort_tbl; rel_tbl; obj_tbl; conclno_tbl; conclno_hyp_tbl; name_tbl]; + List.iter del_from tables_to_clean; owned_uris +let unindex ~dbd ~uri = + let uri = UriManager.string_of_uri uri in + let del_from tbl = + let query tbl = + sprintf "DELETE FROM %s WHERE source LIKE \"%s%%\"" (tbl ()) uri + in + ignore (Mysql.exec dbd (query tbl)) + in + List.iter del_from tables_to_clean + diff --git a/helm/ocaml/metadata/metadataDb.mli b/helm/ocaml/metadata/metadataDb.mli index 17d6fc094..a5b0d2753 100644 --- a/helm/ocaml/metadata/metadataDb.mli +++ b/helm/ocaml/metadata/metadataDb.mli @@ -44,3 +44,5 @@ val index_inductive_def: * @return list of uris removed from the db *) val clean: dbd:Mysql.dbd -> string list +val unindex: dbd:Mysql.dbd -> uri:UriManager.uri -> unit +