From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 10 Jul 2007 15:15:33 +0000 (+0000)
Subject: fixed a bug in the cleanup ofsedir that was not properly catching #xpointer
X-Git-Tag: 0.4.95@7852~355
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d9ddb66a03d6e70a7fa9f99a7f513e2149e25e99;p=helm.git

fixed a bug in the cleanup ofsedir that was not properly catching #xpointer
---

diff --git a/components/library/libraryClean.ml b/components/library/libraryClean.ml
index e137c1873..7a4168402 100644
--- a/components/library/libraryClean.ml
+++ b/components/library/libraryClean.ml
@@ -98,29 +98,24 @@ let db_uris_of_baseuri buri =
   let obj_tbl = MetadataTypes.name_tbl () in
   if HSql.isMysql dbtype dbd then        
     sprintf ("SELECT source FROM %s WHERE " 
-    ^^ "source REGEXP '^%s[^/]*$'") obj_tbl buri
+    ^^ "source REGEXP '^%s[^/]*(#xpointer.*)?$'") obj_tbl buri
   else
    begin
     sprintf ("SELECT source FROM %s WHERE " 
-      ^^ "REGEXP(source, '^%s[^/]*$')") obj_tbl buri
-     (* implementation with vanilla ocaml-sqlite3
-    HLog.debug "Warning SELECT without REGEXP";
-    sprintf
-    ("SELECT source, h_occurrence FROM %s WHERE " ^^ 
-    "h_occurrence LIKE '%s%%' " ^^ HSql.escape_string_for_like)
-    obj_tbl buri
-    *)
+      ^^ "REGEXP(source, '^%s[^/]*(#xpointer.*)?$')") obj_tbl buri
    end
  in
  try 
   let rc = HSql.exec dbtype dbd query in
+  let strip_xpointer s = Pcre.replace ~pat:"#.*$" s in
   let l = ref [] in
   HSql.iter rc (
     fun row -> 
       match row.(0) with 
-      | Some uri when Filename.dirname uri = buri -> 
+      | Some uri when Filename.dirname (strip_xpointer uri) = buri -> 
           l := uri :: !l
-      | _ -> ());
+      | _ ->
+          ());
   let l = List.sort Pervasives.compare !l in
   HExtlib.list_uniq l
  with
@@ -170,7 +165,9 @@ let close_uri_list uri_to_remove =
   in
   let uri_to_remove_from_db =
    List.fold_left 
-     (fun acc buri -> db_uris_of_baseuri buri @ acc
+     (fun acc buri -> 
+       let dbu = db_uris_of_baseuri buri in
+       dbu @ acc
      ) [] buri_to_remove 
   in
   let uri_to_remove = uri_to_remove @ uri_to_remove_from_db in